Introducing Functional Programmers to Interactive Theorem Proving and Program Verification Teaching Experience Report

摘要: We report on the design and preliminary evaluation of a short introductory course interactive theorem proving program verification using Coq proof assistant, targeted at students with background in functional programming software engineering. The builds concepts familiar from to develop understanding logic mechanized by means Curry-Howard isomorphism. A particular emphasis is made computational nature decidable properties various data structures. This approach practical importance, as Coq’s normalization can automatically simplify or discharge such properties, thus reducing burden constructing proofs hand. As basis for teaching this style mechanization, we use Gonthier et al.’s Ssreflect extension its associated libraries. In course, minimize exposure ad-hoc automation via tactics, request that only small set proof-building primitives they should clearly understand. addition introducing an application programming, topics covered include: implementation custom rewriting principles instances indexed type families, boolean reflection, algebraic structures inheritance between them, imperative programs separation Hoare Type Theory.