Chapter 18: The Program Tactic
Catherine ParentThe facilities described in this document pertain to a special aspect of the Coq system: how to associate to a functional program, whose specification is written in Gallina, a proof of its correctness.
This methodology is based on the Curry-Howard isomorphism between functional programs and constructive proofs. This isomorphism allows the synthesis of a functional program from the constructive part of its proof of correctness. That is, it is possible to analyze a Coq proof, to erase all its non-informative parts (roughly speaking, removing the parts pertaining to sort Prop, considered as comments, to keep only the parts pertaining to sort Set).
This realizability interpretation was defined by Christine Paulin-Mohring in her PhD dissertation, and implemented as a program extraction facility in previous versions of Coq by Benjamin Werner. However, the corresponding certified program development methodology was very awkward: the user had to understand very precisely the extraction mechanism in order to guide the proof construction towards the desired algorithm. The facilities described in this chapter attempt to do the reverse: i.e. to try and generate the proof of correctness from the program itself, given as argument to a specialized tactic. This work is based on the PhD dissertation of Catherine Parent (see bibliography of the Coq reference manual).
- 18.1 Developing certified programs: Motivations
- 18.2 Using Program
- 18.3 Syntax for programs
- 18.4 Examples