Extending type theory with forcing

DOI10.1109/LICS.2012.49MaRDI QIDQ2986815zbMATH OpenFDO

Authors Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau

Publication date 16 May 2017

Published in 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/LICS.2012.49

zbMATH Keywords

Coqforcingpresheavestype theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Other aspects of forcing and Boolean-valued models (03E40) Categorical logic, topoi (03G30)

Recommendations

• The definitional side of the forcing
• A computational interpretation of forcing in type theory
• A note on forcing and type theory
• The calculus of constructions
• scientific article; zbMATH DE number 1420782

Cited in

(9)

• Failure is not an option. An exceptional type theory
• Realizability models for a linear dependent PCF
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• A note on forcing and type theory
• The definitional side of the forcing
• Higher order functions and Brouwer's thesis
• A computational interpretation of forcing in type theory
• Constructive modalities with provability smack
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Extending type theory with forcing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2986815)