Title
An Introduction To Small Scale Reflection In Coq
Abstract
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.
Year
Venue
DocType
2010
JOURNAL OF FORMALIZED REASONING
Journal
Volume
Issue
ISSN
3
2
1972-5787
Citations 
PageRank 
References 
33
1.42
1
Authors
2
Name
Order
Citations
PageRank
Georges Gonthier12275195.06
Assia Mahboubi230820.84