Extending Dependent Type Theory with Forcing

Guilhem Jaber

Forcing has been introduced by P. Cohen to prove the independence of the Continuum Hypothesis in Set Theory. While generally considered as a semantic construction, it can also be seen syntactically as a proof translation.

In this talk, we will present such forcing proof translations, for the Calculus of Constructions, a dependent type theory which is the foundation of the proof assistant Coq. Using them, we can extend the logic behind Coq with new principles, while keeping its fundamental properties: soundness, canonicity and decidability of type-checking. Furthermore, following the Curry-Howard proof/program correspondence, this also gives us, as we will see, a computational interpretation of forcing that corresponds to a "monotonic" version of the reader monad.

So we will first consider a forcing translation coming from the restatement of forcing as (pre)sheaves models. However, this translation suffers from coherence problems. By decomposing this translation using P. Levy's call-by-push-value, we will see that this translation is call-by-value, but that there exists an other, more mysterious, call-by-name forcing translation, which does not suffer from such coherence problems.

This is joint work with G. Lewertowski, P.-M. Pedrot, M. Sozeau and N. Tabareau