Wiki Agenda Contact Version française

Publications : Matthieu Sozeau

[9] Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq coq correct! verification of type checking and erasure for coq, in coq. Proc. ACM Program. Lang., 4(POPL), December 2019. [ bib | DOI | http ]
Keywords: type checker, certification, proof assistants
[8] Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. Thèse de doctorat, Université Paris-Sud, December 2008. [ bib ]
[7] Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In Otmame Aït-Mohamed, César Muñoz, and Sofiène Tahar, editors, 21th International Conference on Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science. Springer, August 2008. [ bib | Slides | .pdf ]
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.

[6] Matthieu Sozeau. User defined equalities and relations, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2. [ bib ]
[5] Matthieu Sozeau. Program, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2, [ bib | http ]
[4] Matthieu Sozeau. Type Classes. INRIA, 2008. Chapter of The Coq Proof Assistant Reference Manual -- Version V8.2. [ bib ]
[3] Matthieu Sozeau. Subset coercions in Coq. In Thorsten Altenkirch and Conor Mc Bride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 237--252. Springer, 2007. [ bib | Slides | .pdf ]
We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming 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 mathematical convention. The typing judgements can be translated to the Calculus of Inductive Constructions 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.

[2] Matthieu Sozeau. Program-ing finger trees in Coq. In Ralf Hinze and Norman Ramsey, editors, 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, pages 13--24, Freiburg, Germany, 2007. ACM Press. [ bib | DOI | Slides | .pdf ]
Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent data structure with good performance. Their genericity permits developing a wealth of structures like ordered sequences or interval trees on top of a single implementation. However, the type systems used by current functional languages do not guarantee the coherent parameterization and specialization of Finger Trees, let alone the correctness of their implementation. We present a certified implementation of Finger Trees solving these problems using the Program extension of Coq. We not only implement the structure but also prove its invariants along the way, which permit building certified structures on top of Finger Trees in an elegant way.

[1] Matthieu Sozeau. Coercion par prédicats en Coq. Master's thesis, Université Paris 7, 2005. In French. [ bib | .pdf ]

This page was generated by bibtex2html.