A note on forcing and type theory

DOI10.3233/FI-2010-262zbMATH Open1239.03041MaRDI QIDQ3065010FDOQ3065010

Authors: Thierry Coquand, Guilhem Jaber 

Publication date: 3 January 2011

Published in: Fundamenta Informaticae (Search for Journal in Brave)

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

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)

Cited In (12)

• Title not available (Why is that?)
• Extending type theory with forcing
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Continuity of Gödel's system T definable functionals via effectful forcing
• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• A computational interpretation of forcing in type theory
• A Note on Shoenfield's Unramified Forcing
• A constructive model of uniform continuity
• Validating Brouwer's continuity principle for numbers using named exceptions
• Forcing and the Omitting Types Theorem For Lt
• The definitional side of the forcing
• Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally

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)