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

• Title: Textual Explanation of Proof for Calculus of Inductive Constructions
• Author: Yann Coscoy.
• Supervisors: Yves Bertot et Gilles Kahn.
• Postscript file.
• BibTex entry:
  

  @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"}
  }

• Abstract:

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.

Remark

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

Publications

• A translation of proofs (-termes) of Calculus of Constructions into natural language (english):
  • Yann Coscoy, Gilles Kahn, and Laurent Théry
    Extracting Text from Proof
    Typed Lambda-Calculi and Applications (TLCA `95), Springer-Verlag LNCS 905, Edinburgh, April 1995.
    
  • Postscript file.
  • BibTex entry:
    

    @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"}
    }

• An improvement of previous paper focusing on proof relevancy:
  • Yann Coscoy,
    A Natural Language Explanation for Formal Proofs
    Logical Aspects of Computational Linguistics (LACL'96), Springer-Verlag LNAI 1328, Nancy, September 1996.
    
  • Postscript file.
  • BibTex entry:
    

    @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"}
    }

• New homepage: http://yann.coscoy.free.fr/
• E-mail: Yann.Coscoy@free.fr