Kripke Semantics for Martin-Löf’s Extensional Type Theory

DOI10.1007/978-3-642-02273-9_19zbMath1246.03022OpenAlexW64194158MaRDI QIDQ3637199

Florian Rabe, Steven Awodey

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_19

Mathematics Subject Classification ID

Related Items

J-Calc: a typed lambda calculus for intuitionistic justification logic, Representing Model Theory in a Type-Theoretical Logical Framework

Cites Work

• Kripke-style models for typed lambda calculus
• Alpha conversion, conditions on variables and categorical logic
• Generalized algebraic theories and contextual categories
• Sheaves in geometry and logic: a first introduction to topos theory
• Categorical logic and type theory
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• Locally cartesian closed categories and type theory
• Adjointness in Foundations
• Kripke semantics for dependent type theory and realizability interpretations
• A formulation of the simple theory of types
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item