A generalization of the Takeuti–Gandy interpretation
From MaRDI portal
Publication:5740650
DOI10.1017/S0960129514000504zbMath1362.03005MaRDI QIDQ5740650
Bruno Barras, Thierry Coquand, Simon Huber
Publication date: 27 July 2016
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Related Items (4)
Homotopical patch theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ A Kripke model for simplicial sets ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction
Cites Work
- Unnamed Item
- Proof-relevance of families of setoids and identity in type theory
- Constructivism in mathematics. An introduction. Volume I
- A course in constructive algebra
- On the axiom of extensionality – Part I
- Homotopy theoretic models of identity types
- Logical relations and the typed λ-calculus
- L.J.E. Brouwer : Topologie et constructivisme
- Intensional interpretations of functionals of finite type I
- A formulation of the simple theory of types
This page was built for publication: A generalization of the Takeuti–Gandy interpretation
