Metodo

International Studies in Phenomenology and Philosophy

Book | Chapter

186518

A computational interpretation of forcing in type theory

Thierry Coquand Guilhem Jaber

pp. 203-213

Abstract

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

Published in:

Dybjer P, Lindström Sten, Palmgren Erik, Sundholm Göran (2012) Epistemology versus ontology: essays on the philosophy and foundations of mathematics in honour of per Martin-löf. Dordrecht, Springer.

Pages: 203-213

DOI: 10.1007/978-94-007-4435-6_10

Full citation:

Coquand Thierry, Jaber Guilhem (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, 203–213.