Forcing in Coq

Matthieu Sozeau 1, 2 Nicolas Tabareau 3, 4 Guilhem Jaber 3, 4
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
2 PPS - Preuves, Programmes et Systèmes
3 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes Atlantique
4 LINA - Laboratoire d'Informatique de Nantes Atlantique
Document type :
Other publications
Complete list of metadatas
https://hal.inria.fr/hal-00767483
Contributor : Matthieu Sozeau <>
Submitted on : Thursday, December 20, 2012 - 1:57:36 AM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM

Identifiers

  • HAL Id : hal-00767483, version 1

Collections

UNIV-PARIS7 | INRIA | PPS | INFO | LINA-ASCOLA | LINA | UNIV-NANTES | USPC | INRIA-ROCQ | IMT-ATLANTIQUE

Citation

Matthieu Sozeau, Nicolas Tabareau, Guilhem Jaber. Forcing in Coq. 2012. ⟨hal-00767483⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

327

Contact


archive-ouverte@inria.fr