Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00077191
Contributor : Rapport de Recherche Inria <>
Submitted on : Monday, May 29, 2006 - 5:16:39 PM
Last modification on : Saturday, January 27, 2018 - 1:31:35 AM
Long-term archiving on: : Friday, May 13, 2011 - 10:49:56 PM

Identifiers

  • HAL Id : inria-00077191, version 1

Collections

Citation

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

Share

Metrics

Record views

139

Files downloads

84