scientific article; zbMATH DE number 4047723

zbMATH Open0643.03050MaRDI QIDQ3784072FDOQ3784072

Authors: Thierry Coquand, Thomas Ehrhard 

Publication date: 1987

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

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)

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)

Cited In (14)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Infinite hypergraphs. I: Basic properties
• Categories of embeddings
• Comparing higher-order encodings in logical frameworks and tile logic
• Inheritance as implicit coercion
• Title not available (Why is that?)
• 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)
• Title not available (Why is that?)

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)