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.
@PHDTHESIS{Thesis, author = {Y. Coscoy}, title = {{E}xplication textuelles de preuves pour le calcul des constructions inductives}, school = {{U}niversité de {N}ice-{S}ophia-{A}ntipolis}, type = {Thèse d'université}, year = {2000}, month = {September}, url = {"http://www-sop.inria.fr/lemme/Yann.Coscoy/these.ps"} }
This thesis is about presentation of proofs in the formalism of Calculus of Inductive Constructions.
The Calculus of Constructions is a typed -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 -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 -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.
@INPROCEEDINGS{TLCA, author = {Y. Coscoy and G. Kahn and L. Théry}, title = {Extracting Text from Proof}, booktitle = {Proceedings of Int. Conf. on Typed Lambda-Calculus and Applications ({TLCA}), Edinburgh}, editor = {M. Dezani and G. Plotkin}, publisher = {Springer-Verlag {LNCS}}, volume = {902}, year = {1995}, month = {April}, url = {"http://www-sop.inria.fr/lemme/Yann.Coscoy/tlca95.ps"} }
@INPROCEEDINGS{LACL, author = {Y. Coscoy}, title = {A Natural Language Explanation for Formal Proofs}, booktitle = {Proceedings of Int. Conf. on Logical Aspects of {C}omputational Liguistics ({LACL}), Nancy}, editor = {C. Retoré}, publisher = {Springer-Verlag LNCS/LNAI}, volume = {1328}, year = {1996}, month = {September}, url = {"http://www-sop.inria.fr/lemme/Yann.Coscoy/lacl96.ps"} }