version française

Yann Coscoy

Yann Coscoy have done a Phd thesis at INRIA in Lemme team (was CROAP) from 1995 to 1999. Supervisors were Yves Bertot and de Gilles Kahn.

PhD thesis

This thesis is about presentation of proofs in the formalism of Calculus of Inductive Constructions.

  The Calculus of Constructions is a typed lambda-calculus introduced by Th. Coquand and G. Huet. It allows a functional encoding of high order proofs using Curry-Howard Isomorphism. In this thesis, we study an extension of this formalism by Ch. Paulin and B. Werner.

  We describe a reversible function that translates a formal proof into a french mathematical text. In this direction, from lambda-term\ into natural language, this function is a proof presentation. It proceeds by selecting information, organizing the speech then verbalizing. In the other direction, from text into lambda-term, it is a validation. The text is syntaxically analysed then evaluated as a proof system script.

  The reversibility of the translation guarantees that the texts generated into french are formal proofs. They are indeed validable by a fully automatic process.


A not so technical overview of this work in avaible online (in french) here.