An introduction to small scale reflection in Coq

Georges Gonthier, Assia Mahboubi


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.

Full Text:

PDF (English)

DOI: 10.6092/issn.1972-5787/1979

Copyright (c) 2010 Georges Gonthier, Assia Mahboubi

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 International License.
This website uses only proprietary and third party technical cookies to ensure the correct operation of its web pages and to improve its services. If you wish to find out more, or deny your consent, consult the privacy policy. By continuing to navigate the website, or by clicking on "close", you consent to the use of the cookies.

ISSN 1972-5787

Creative Commons License
© Copyright 2016

The journal is hosted and mantained by ASDD-AlmaDL [privacy]