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 : mardi 17 avril 2018 - 11:33:08

Identifiants

  • HAL Id : hal-00767483, version 1

Collections

INRIA | PPS | INFO | UNIV-NANTES | LINA | LINA-ASCOLA | USPC | IMTA | INRIA-RENGRE

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

266

Contact


archive-ouverte@inria.fr