Yann Coscoy a effectué une thèse à l'INRIA au sein du projet Lemme (anciennement CROAP) entre 1995 et 1999. Ce travail était placé sous la direction de Yves Bertot et de Gilles Kahn.
Yann Coscoy have done a Phd thesis « Textual Explanation of Proof for Calulus of Inductive Constructions ». This work took place in INRIA in team Lemme (was CROAP). 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"}
}
Ce travail concerne la présentation des preuves formalisées dans le calcul des constructions inductives.
Le calcul des constructions est un 
-calcul typé introduit par Th. Coquand et G. Huet. Il
permet un codage fonctionnel des preuves d'ordre supérieur par
l'isomorphisme de Curry-Howard. Nous étudions dans ce manuscrit une
variante de ce formalisme étendue par Ch. Paulin et B. Werner.
Nous décrivons une fonction réversible traduisant les termes de
preuve du formalisme en des textes mathématiques en français. Dans
le premier sens, du -terme vers la langue naturelle, cette traduction est une
présentation de la preuve. Elle comporte une phase de sélection des
information avec organisation du discourt puis une phase de
verbalisation. Dans l'autre sens, du texte vers le -terme, il s'agit d'une
validation. Le texte est analysé syntaxiquement puis évalué comme un
script de système de preuve.
La réversibilité de la fonction de présentation permet de garantir formellement que les démonstrations produites en français sont des preuves formelles. Elles peuvent de fait être validées par un processus automatique.
Un aperçu peu technique des travaux effectués au cours de cette thèse est disponible en ligne ici.
-termes)
du calcul des constructions en langue naturelle (anglais) :
@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"}
}