A generalization of the Takeuti-Gandy interpretation
From MaRDI portal
Publication:5740650
DOI10.1017/S0960129514000504zbMATH Open1362.03005MaRDI QIDQ5740650FDOQ5740650
Authors: Bruno Barras, Thierry Coquand, Simon Huber 
Publication date: 27 July 2016
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Recommendations
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- scientific article; zbMATH DE number 2079044
- The simplicial model of univalent foundations (after Voevodsky)
- Revisiting the categorical interpretation of dependent type theory
- The generalised type-theoretic interpretation of constructive set theory
Cites Work
- Constructivism in mathematics. An introduction. Volume I
- Title not available (Why is that?)
- A course in constructive algebra
- Homotopy theoretic models of identity types
- Logical relations and the typed λ-calculus
- A formulation of the simple theory of types
- Intensional interpretations of functionals of finite type I
- Proof-relevance of families of setoids and identity in type theory
- On the axiom of extensionality – Part I
- L.J.E. Brouwer : Topologie et constructivisme
Cited In (8)
- Stack semantics of type theory
- Homotopical patch theory
- Normalization by Evaluation for Typed Weak lambda-Reduction
- The generalised type-theoretic interpretation of constructive set theory
- Towards a constructive simplicial model of Univalent Foundations
- A dependently-typed construction of semi-simplicial types
- A Kripke model for simplicial sets
- Refinement by Interpretation in a General Setting
This page was built for publication: A generalization of the Takeuti-Gandy interpretation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740650)
