Alpha conversion, conditions on variables and categorical logic

DOI10.1007/BF00370828zbMath0701.03036MaRDI QIDQ913792

Pierre-Louis Curien

Publication date: 1989

Published in: Studia Logica (Search for Journal in Brave)

zbMATH Keywords

dependent typesindexed categories\(\lambda \) -calculuscategorical combinatorscategories-as-syntaxcontextual categoriesdescription of quantifiers as adjointsequational presentationsequent formulation of natural deduction

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items

Comprehension categories and the semantics of type dependency, Kripke Semantics for Martin-Löf’s Extensional Type Theory, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The system \({\mathcal F}\) of variable types, fifteen years later
• The categorical abstract machine
• Unique normal forms for lambda calculus with surjective pairing
• Proof of termination of the rewriting system SUBSET on CCL
• Domain theoretic models of polymorphism
• Locally cartesian closed categories and type theory
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Categorical combinators
• Categorical semantics for higher order polymorphic lambda calculus
• On the geometry of spaces of $C_{0}$K-valued operators
• Constructive natural deduction and its ‘ω-set’ interpretation
• Adjointness in Foundations
• The Mechanical Evaluation of Expressions