A Computational Interpretation of Forcing in Type Theory

DOI10.1007/978-94-007-4435-6_10zbMath1312.03021OpenAlexW139012711MaRDI QIDQ5253929

Guilhem Jaber, Thierry Coquand

Publication date: 5 June 2015

Published in: Epistemology versus Ontology (Search for Journal in Brave)

Full work available at URL: https://halshs.archives-ouvertes.fr/halshs-00775352/file/KantAndRealNumbers-separatum.pdf

zbMATH Keywords

type theorycomputational interpretation of forcing

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40) Other aspects of forcing and Boolean-valued models (03E40)

Related Items (6)

Continuity of Gödel's system T definable functionals via effectful forcing ⋮ A constructive manifestation of the Kleene-Kreisel continuous functionals ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Higher order functions and Brouwer’s thesis

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On a hitherto unexploited extension of the finitary standpoint
• Constructivism in mathematics. An introduction. Volume II
• The discovery of forcing.
• A Note on Forcing and Type Theory
• Relativized realizability in intuitionistic arithmetic of all finite types
• The Impact of the Lambda Calculus in Logic and Computer Science

This page was built for publication: A Computational Interpretation of Forcing in Type Theory