Subset coercions in Coq

Abstract. We propose a new language for writing programs with de-pendent types which can be elaborated into partial Coq terms. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means al-lowing to write algorithms as easily as in a practical functional program-ming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the “Predicate subtyping ” feature of PVS and following mathemat-ical convention. The typing judgements can be translated to the Calcu-lus of (Co-)Inductive Constructions (Cic) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment.