A Small Scale Reflection Extension for the Coq system

Georges Gonthier 1, 2 Assia Mahboubi 2, 3
3 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : 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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00258384
Contributor : Assia Mahboubi <>
Submitted on : Monday, July 27, 2009 - 4:52:59 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Thursday, September 23, 2010 - 5:20:27 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00258384, version 3

Citation

Georges Gonthier, Assia Mahboubi. A Small Scale Reflection Extension for the Coq system. [Research Report] RR-6455, 2008. ⟨inria-00258384v3⟩

Share

Metrics

Record views

69

Files downloads

27