文章基本信息

标题：An introduction to small scale reflection in Coq
本地全文：下载
作者：Georges Gonthier ; Assia Mahboubi
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2010
卷号：3
期号：2
页码：95-152
DOI：10.6092/issn.1972-5787/1979
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：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.