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
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
4 LINA - Laboratoire d'Informatique de Nantes Atlantique
Type de document :
Autre publication
A plugin for Coq that implements a generic Forcing translation for any given set of conditions. I.. 2012
Liste complète des métadonnées
https://hal.inria.fr/hal-00767483
Contributeur : Matthieu Sozeau <>
Soumis le : jeudi 20 décembre 2012 - 01:57:36
Dernière modification le : vendredi 4 janvier 2019 - 17:33:25

Identifiants

  • HAL Id : hal-00767483, version 1

Collections

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

Citation

Matthieu Sozeau, Nicolas Tabareau, Guilhem Jaber. Forcing in Coq. A plugin for Coq that implements a generic Forcing translation for any given set of conditions. I.. 2012. 〈hal-00767483〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

309

Contact


archive-ouverte@inria.fr