scientific article; zbMATH DE number 4177054

MaRDI QIDQ3201049zbMATH OpenFDO

Authors Pierre-Louis Curien

Publication date 1990

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

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)

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

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 4047723 (Why is no real title available?)
• scientific article; zbMATH DE number 4048997 (Why is no real title available?)
• scientific article; zbMATH DE number 3779585 (Why is no real title available?)
• scientific article; zbMATH DE number 125886 (Why is no real title available?)
• scientific article; zbMATH DE number 4118557 (Why is no real title available?)
• scientific article; zbMATH DE number 4120168 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 4187810 (Why is no real title available?)
• A 2-categorical pasting theorem
• Adjointness in Foundations
• Alpha conversion, conditions on variables and categorical logic
• Categorical and algebraic aspects of Martin-Löf type theory
• Coherence for bicategories and indexed categories
• Locally cartesian closed categories and type theory
• On the geometry of spaces of $C_{0}$K-valued operators
• Proof of termination of the rewriting system SUBSET on CCL
• The categorical abstract machine

Cited in

(7)

• The Substitution Vanishes
• Simultaneous substitution in the typed lambda calculus
• scientific article; zbMATH DE number 445156 (Why is no real title available?)
• 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)