A Note on Forcing and Type Theory
From MaRDI portal
Publication:3065010
DOI10.3233/FI-2010-262zbMATH Open1239.03041MaRDI QIDQ3065010
Thierry Coquand, Guilhem Jaber
Publication date: 3 January 2011
Published in: Fundamenta Informaticae (Search for Journal in Brave)
continuityforcingconstructive mathematicsMartin-Löf type theoryintuitionistic type theory, dependent types
Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Other aspects of forcing and Boolean-valued models (03E40)
Related Items (9)
Continuity of Gödel's system T definable functionals via effectful forcing ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Forcing and the Omitting Types Theorem For Lt ⋮ A Note on Shoenfield's Unramified Forcing ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally ⋮ \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity ⋮ Title not available (Why is that?) ⋮ A Computational Interpretation of Forcing in Type Theory
This page was built for publication: A Note on Forcing and Type Theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3065010)
