The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources. This paper introduces a typed functional language Lambda! and a categorical model for it. The terms of Lambda! encode a version of natural deduction for Intuitionistic Linear Logic such that linear and non linear assumptions are managed multiplicatively and additively, respectively. Correspondingly, the terms of Lambda! are built out of two disjoint sets of variables. Moreover, the lambda-abstractions of Lambda! bind variables and patterns. The use of two different kinds of variables and the patterns allow a very compact definition of the one-step operational semantics of Lambda!, unlike all other extensions of Curry-Howard Isomorphism to Intuitionistic Linear Logic. The language Lambda! is Church-Rosser and enjoys both Strong Normalizability and Subject Reduction. The categorical model induces operational equivalences like, for example, a set of extensional equivalences. The paper presents also an untyped version of Lambda! and a type assignment for it, using formulas of Linear Logic as types. The type assignment inherits from Lambda! all the good computational properties and enjoys also the Principal-Type Property.

Lambda Calculus and Intuitionistic Linear Logic

RONCHI DELLA ROCCA, Simonetta;ROVERSI, Luca
1997-01-01

Abstract

The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources. This paper introduces a typed functional language Lambda! and a categorical model for it. The terms of Lambda! encode a version of natural deduction for Intuitionistic Linear Logic such that linear and non linear assumptions are managed multiplicatively and additively, respectively. Correspondingly, the terms of Lambda! are built out of two disjoint sets of variables. Moreover, the lambda-abstractions of Lambda! bind variables and patterns. The use of two different kinds of variables and the patterns allow a very compact definition of the one-step operational semantics of Lambda!, unlike all other extensions of Curry-Howard Isomorphism to Intuitionistic Linear Logic. The language Lambda! is Church-Rosser and enjoys both Strong Normalizability and Subject Reduction. The categorical model induces operational equivalences like, for example, a set of extensional equivalences. The paper presents also an untyped version of Lambda! and a type assignment for it, using formulas of Linear Logic as types. The type assignment inherits from Lambda! all the good computational properties and enjoys also the Principal-Type Property.
1997
59(3)
417
448
http://www.di.unito.it/~rover/
S. RONCHI DELLA ROCCA; L. ROVERSI
File in questo prodotto:
File Dimensione Formato  
RonchiRoversi1997STUDIALOGICA.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 247.51 kB
Formato Adobe PDF
247.51 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/41226
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact