inria-00258384, version 10
A Small Scale Reflection Extension for the Coq system
Georges Gonthier
1Assia Mahboubi
1, 2Enrico Tassi 1
N° RR-6455 (2008)
Résumé : This document describes a set of extensions to the proof scripting language of the Coq proof assistant. While these extensions were developed to support a particular proof methodology - small-scale reflection - most of them actually are of a quite general nature, improving the functionality of Coq in basic areas such as script layout and structuring, proof context management, and rewriting. Consequently, and in spite of the title of this document, most of the extensions described here should be of interest for all Coq users, whether they embrace small-scale reflection or not.
- 1 : Microsoft Research - Inria Joint Centre (MSR - INRIA)
- INRIA – Microsoft – Microsoft Research Laboratory Cambridge
- 2 : TypiCal (INRIA Saclay - Ile de France)
- INRIA – CNRS : UMR – Polytechnique - X
- Domaine : Informatique/Logique en informatique
- Référence interne : RR-6455
- Versions disponibles : v1 (22-02-2008) v2 (28-02-2008) v3 (28-07-2009) v4 (07-08-2009) v5 (21-02-2011) v6 (12-03-2011) v7 (15-03-2011) v8 (16-03-2011) v9 (16-03-2011) v10 (29-03-2011)
- inria-00258384, version 10
- http://hal.inria.fr/inria-00258384
- oai:hal.inria.fr:inria-00258384
- Contributeur : Assia Mahboubi
- Soumis le : Lundi 28 Mars 2011, 17:10:48
- Dernière modification le : Mardi 29 Mars 2011, 10:34:35






Documents associés
Exporter