An introduction to small scale reflection in Coq
AbstractThis 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.
How to Cite
Gonthier, G., & Mahboubi, A. (2010). An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2), 95–152. https://doi.org/10.6092/issn.1972-5787/1979
Copyright (c) 2010 Georges Gonthier, Assia Mahboubi
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy