Introducing modularity and sharing in a typed Lambda-calculus

Abstract : Thanks to the Curry-Howard isomorphism, typed lambda-calculi provide a convenient logical framework to formalize the concept of proof. The large size of proofs dictates the introduction of concepts of struturation and modularity. This in turn raises the problem of information sharing between modules. This paper presents the results of such a study for a language derived from Nederpelt'system Y. We first discuss the reasons why sharing is not correctly supported and then a new calculus is proposed, which allows the definition of modules. This calculus provides a mechanism of access between modules that let them share information. It is defined in terms of an operational semantics and a comparison with the system Y is provided.
Type de document :
[Research Report] RR-1903, INRIA. 1993
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 17:16:39
Dernière modification le : samedi 27 janvier 2018 - 01:31:35
Document(s) archivé(s) le : vendredi 13 mai 2011 - 22:49:56



  • HAL Id : inria-00077191, version 1



Alain Costes. Introducing modularity and sharing in a typed Lambda-calculus. [Research Report] RR-1903, INRIA. 1993. 〈inria-00077191〉



Consultations de la notice


Téléchargements de fichiers