Extracting Text from Proofs

Yann Coscoy 1 Gilles Kahn Laurent Thery
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In this paper, we propose a method for presenting formal proofs in an intelligible form. We describe a transducer from proof objects ($\lambda$-terms in the Calculus of Constructions) to pseudo natural language that has been implemented for the Coq system
Type de document :
Rapport
RR-2459, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074217
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:47:43
Dernière modification le : samedi 27 janvier 2018 - 01:31:28
Document(s) archivé(s) le : mardi 12 avril 2011 - 16:07:10

Fichiers

Identifiants

  • HAL Id : inria-00074217, version 1

Collections

Citation

Yann Coscoy, Gilles Kahn, Laurent Thery. Extracting Text from Proofs. RR-2459, INRIA. 1995. 〈inria-00074217〉

Partager

Métriques

Consultations de la notice

94

Téléchargements de fichiers

192