An introduction to small scale reflection in Coq

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 distrib...

Повний опис

Бібліографічні деталі
Автори: Georges Gonthier, Assia Mahboubi
Формат: Стаття
Мова:English
Опубліковано: University of Bologna 2010-01-01
Серія:Journal of Formalized Reasoning
Онлайн доступ:http://jfr.cib.unibo.it/article/view/1979/1358