CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A computational interpretation of forcing in type theory

Thierry Coquand (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)) ; G. Jaber
Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of per Martin-Löf p. 203-213. (2012)
[Kapitel]

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.



Denna post skapades 2017-10-30.
CPL Pubid: 252829

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)