scientific article; zbMATH DE number 4177054

zbMATH Open0715.03029MaRDI QIDQ3201049FDOQ3201049

Authors: Pierre-Louis Curien 

Publication date: 1990

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

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 445156
• Invertible substitutions and local isomorphisms
• On the Notion of Substitution
• scientific article; zbMATH DE number 590283
• Higher-order substitutions
• Explicit substitutions
• Explicit substitutions and reducibility
• Axiomatisation of substitution
• scientific article; zbMATH DE number 458878

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

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

Cites Work

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

Cited In (7)

• The Substitution Vanishes
• Simultaneous substitution in the typed lambda calculus
• Title not available (Why is that?)
• Higher-dimensional word problems with applications to equational logic
• Products of families of types and (Pi,lambda)-structures on C-systems
• Multimodal dependent type theory
• An interpretation of dependent type theory in a model category of locally cartesian closed categories

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3201049)