Extending Type Theory with Forcing
In: LICS 2012 : Logic In Computer Science ; https://hal.science/hal-00685150 ; LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0, 2012
Online
Konferenz
Zugriff:
International audience ; This paper presents an intuitionistic forcing translation for the Calculus of Constructions (CoC), a translation that corresponds to an internalization of the presheaf construction in CoC. Depending on the chosen set of forcing conditions, the resulting type system can be extended with extra logical principles. The translation is proven correct-in the sense that it preserves type checking-and has been implemented in Coq. As a case study, we show how the forcing translation on integers (which corresponds to the internalization of the topos of trees) allows us to define general inductive types in Coq, without the strict positivity condition. Using such general inductive types, we can construct a shallow embedding of the pure \lambda-calculus in Coq, without defining an axiom on the existence of an universal domain. We also build another forcing layer where we prove the negation of the continuum hypothesis.
Titel: |
Extending Type Theory with Forcing
|
---|---|
Autor/in / Beteiligte Person: | Jaber, Guilhem ; Tabareau, Nicolas ; Sozeau, Matthieu ; Aspect and composition languages (ASCOLA) ; Laboratoire d'Informatique de Nantes Atlantique (LINA) ; Mines Nantes (Mines Nantes)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS)-Mines Nantes (Mines Nantes)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS)-Département informatique -, EMN ; Mines Nantes (Mines Nantes)-Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Université de Nantes (UN)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS) ; Design, study and implementation of languages for proofs and programs ( PI.R2 ) ; Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt ; ANR-11-BS02-0010,RECRE,Réalisabilité pour la logique classique, la concurrence, les références et la réécriture(2011) |
Link: | |
Zeitschrift: | LICS 2012 : Logic In Computer Science ; https://hal.science/hal-00685150 ; LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. pp.0-0, 2012 |
Veröffentlichung: | HAL CCSD, 2012 |
Medientyp: | Konferenz |
Schlagwort: |
|
Sonstiges: |
|