Sala Riunioni 1 - Dipartimento di Scienze dell'Informazione - at 15.00

Title
"Procedural Representation of CIC Proof Terms"


Abstract

The generation of procedural proof scripts from CIC proof terms is a feature of the formal proof management system Matita developed by A. Asperti and his team in the context of the HELM project.

This feature allows to translate a CIC proof term coming from a digital library or from another proof development system, into an equivalent proof presented in Matita's editable high-level format.

We report on the motivations of this feature, on the current status of its implementation (which is still under development) and on a test case:

762 proof terms generated by Coq 7.3.1 were successfully translated.