Introducing Functional Programmers to Interactive Theorem Proving and Program Verification Teaching Experience Report
Ilya Sergey, Aleksandar Nanevski · 2014
We report on the design and preliminary evaluation of a short introductory course on interactive theorem proving and program verification using the Coq proof assistant, targeted at students with background in functional programming and software engineering. The course builds on concepts familiar from functional pro-gramming to develop understanding of logic and mechanized prov-ing by means of the Curry-Howard isomorphism. A particular em-phasis is made of the computational nature of decidable proper-ties of various data structures. This approach is of practical impor-tance, as Coq’s normalization can automatically simplify or dis-charge such properties, thus reducing the burden of constructing the proofs by hand. As a basis for teaching this style of mecha-nization, we use Gonthier et al.’s Ssreflect extension of Coq and its associated libraries. In the course, we minimize the exposure to ad-hoc proof au-tomation via tactics, and request that students develop proofs us-ing only a small set of proof-building primitives that they should clearly understand. In addition to introducing logic as an applica-tion of functional programming, the topics covered by the course include: implementation of custom rewriting principles as instances of indexed type families, boolean reflection, implementation of al-gebraic structures and inheritance between them, and verification of imperative programs in separation logic and Hoare Type Theory. 1.