scientific article

zbMath0715.03029MaRDI QIDQ3201049

Pierre-Louis Curien

Publication date: 1990

Full work available at URL: https://eudml.org/doc/91749

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

categorical semantics of dependent typescoherence problemsinterpretation of dependent types in a locally Cartesian closed categorymodelling of substitution in types by pullbacks

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30)

Related Items

An interpretation of dependent type theory in a model category of locally cartesian closed categories, Simultaneous substitution in the typed lambda calculus, Higher-dimensional word problems with applications to equational logic, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Categorical and algebraic aspects of Martin-Löf type theory
• A 2-categorical pasting theorem
• Alpha conversion, conditions on variables and categorical logic
• Coherence for bicategories and indexed categories
• The categorical abstract machine
• Proof of termination of the rewriting system SUBSET on CCL
• Locally cartesian closed categories and type theory
• On the geometry of spaces of $C_{0}$K-valued operators
• Adjointness in Foundations