An introduction to small scale reflection in Coq - Archive ouverte HAL Access content directly
Journal Articles Journal of Formalized Reasoning Year : 2010

An introduction to small scale reflection in Coq

(1, 2) , (1, 3, 4)


This tutorial presents the Ssreflect extension to the Coq system. This extension consists of an extension to the Coq language of script, and of a set of libraries, originating from the formal proof of the Four Color theorem. This tutorial proposes a guided tour in some of the basic libraries distributed in the Ssreflect package. It focuses on the application of the small scale reflection methodology to the formalization of finite objects in intuitionistic type theory.
Fichier principal
Vignette du fichier
main-rr.pdf (769.04 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00515548 , version 1 (07-09-2010)
inria-00515548 , version 2 (22-09-2010)
inria-00515548 , version 3 (02-11-2010)
inria-00515548 , version 4 (13-01-2011)


  • HAL Id : inria-00515548 , version 4


Georges Gonthier, Assia Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 2010, 3 (2), pp.95-152. ⟨inria-00515548v4⟩
694 View
1818 Download


Gmail Facebook Twitter LinkedIn More