Extending Type Theory with Forcing

DOI10.1109/LICS.2012.49zbMath1364.03016MaRDI QIDQ2986815

Matthieu Sozeau, Guilhem Jaber, Nicolas Tabareau

Publication date: 16 May 2017

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

zbMATH Keywords

forcingtype theorypresheavesCoq

Mathematics Subject Classification ID

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

Related Items

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, Unnamed Item, Constructive Modalities with Provability Smack, Higher order functions and Brouwer’s thesis, Realizability models for a linear dependent PCF

Uses Software

• Coq