scientific article; zbMATH DE number 4047723

MaRDI QIDQ3784072zbMATH OpenFDO

Authors Thierry Coquand, Thomas Ehrhard

Publication date 1987

zbMATH Keywords

fibrationhigher-order logicindexed categoryequational presentationhigher-order type systempolymorphic \(\lambda \)-calculussemantics of F\(\omega \)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Categorical logic, topoi (03G30) Second- and higher-order arithmetic and fragments (03F35) Fibered categories (18D30)

Recommendations

• Alpha-conversion and typability
• Alpha conversion, conditions on variables and categorical logic
• Publication:4938612
• A combinatory logic approach to higher-order E-unification
• Second-Order Equational Logic (Extended Abstract)

Cited in

(14)

• scientific article; zbMATH DE number 1255555 (Why is no real title available?)
• scientific article; zbMATH DE number 1036757 (Why is no real title available?)
• Infinite hypergraphs. I: Basic properties
• Categories of embeddings
• Comparing higher-order encodings in logical frameworks and tile logic
• Inheritance as implicit coercion
• scientific article; zbMATH DE number 3961694 (Why is no real title available?)
• E-ccc: between ccc and topos, - its expressive power from the viewpoint of data type theory
• Alpha conversion, conditions on variables and categorical logic
• Categorical models of polymorphism
• Domain theoretic models of polymorphism
• Equational methods in first order predicate calculus
• Second-Order Equational Logic (Extended Abstract)
• scientific article; zbMATH DE number 4177054 (Why is no real title available?)

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 Q3784072)