19/2 Matthieu Sozeau (LRI Orsay)

Programming with Dependent Types in Coq

Coq is a mature proof assistant based on a dependent type theory. However, while the use of dependent types is the very basis of all the proofs that are developed in the system, it still requires considerable expertise to tame their full power when programming. We present a solution to alleviate this problem as an additional layer on top of the core type theory that eases programming with strong specifications. We develop a new language inspired by PVS that allows to separate algorithmic and correctness concerns when developing programs with rich types, generating proof obligations on the side in a standard way. We also demonstrate the Program extension to Coq that implements this method on a non-trivial example: Finger Trees. We develop an indexed version of this data structure from which we can derive correct-by-construction priority queues or ropes. This development also illustrates a recently implemented type class extension to Coq.