A note on forcing and type theory

DOI10.3233/FI-2010-262MaRDI QIDQ3065010zbMATH OpenFDO

Authors Thierry Coquand, Guilhem Jaber

Publication date 3 January 2011

Published in Fundamenta Informaticae (Search for Journal in Brave)

zbMATH Keywords

continuityconstructive mathematicsforcingintuitionistic type theory, dependent typesMartin-Löf type theory

Mathematics Subject Classification ID

Other aspects of forcing and Boolean-valued models (03E40) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Recommendations

• A computational interpretation of forcing in type theory
• Continuity of Gödel's system T definable functionals via effectful forcing
• A constructive model of uniform continuity
• Extending type theory with forcing
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation

Cited in

(12)

• A constructive manifestation of the Kleene-Kreisel continuous functionals
• scientific article; zbMATH DE number 7199581 (Why is no real title available?)
• A Note on Shoenfield's Unramified Forcing
• A constructive model of uniform continuity
• Forcing and the Omitting Types Theorem For Lt
• Extending type theory with forcing
• The definitional side of the forcing
• A computational interpretation of forcing in type theory
• Continuity of Gödel's system T definable functionals via effectful forcing
• 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
• Validating Brouwer's continuity principle for numbers using named exceptions

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)