HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, May 29, 2006 - 5:16:39 PM
Last modification on : Friday, February 4, 2022 - 3:15:44 AM
Long-term archiving on: : Friday, May 13, 2011 - 10:49:56 PM


  • 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⟩



Record views


Files downloads