Repository | Book | Chapter
(2012) Epistemology versus ontology, Dordrecht, Springer.
In a previous work, we showed the uniform continuity of definable functionals in intuitionistic type theory as an application of forcing with dependent types. The argument was constructive, and so contains implicitly an algorithm which computes a witness that a given functional is uniformly continuous. We present here such an algorithm, which provides a possible computational interpretation of forcing.
Publication details
DOI: 10.1007/978-94-007-4435-6_10
Full citation:
Coquand, T. , Jaber, G. (2012)., A computational interpretation of forcing in type theory, in P. Dybjer, S. Lindström, E. Palmgren & G. Sundholm (eds.), Epistemology versus ontology, Dordrecht, Springer, pp. 203-213.
This document is unfortunately not available for download at the moment.