CINECA IRIS Institutional Research Information System
IRIS è la piattaforma adottata dall’Università degli Studi di Udine per gestire l’archivio aperto dei prodotti della ricerca. L’archivio contiene articoli, contributi in volume, monografie, interventi pubblicati in atti di convegno, Tesi di dottorato e altri materiali.
EnglishWe propose a type inference algorithm for lambda terms in elementary affine logic (EAL). The algorithm decorates the syntax tree of a simple typed lambda term and collects a set of linear constraints. The result is a parametric elementary type that can be instantiated with any solution of the set of collected constraints. We point out that the typeability of lambda terms in EAL has a practical counterpart, since it is possible to reduce any EAL-typeable lambda terms with the Lamping’s abstract algorithm obtaining a substantial increase of performances. We show how to apply the same techniques to obtain decorations of intuitionistic proofs into linear logic proofs.
Optimizing optimal reduction: A type inference algorithm for elementary affine logic / COPPOLA Paolo; MARTINI Simone. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - (2006), pp. 219-260.
| Titolo: | Optimizing optimal reduction: A type inference algorithm for elementary affine logic | |
| Autori: | ||
| Data di pubblicazione: | 2006 | |
| Rivista: | ||
| Citazione: | Optimizing optimal reduction: A type inference algorithm for elementary affine logic / COPPOLA Paolo; MARTINI Simone. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - (2006), pp. 219-260. | |
| Abstract: | We propose a type inference algorithm for lambda terms in elementary affine logic (EAL). The algorithm decorates the syntax tree of a simple typed lambda term and collects a set of linear constraints. The result is a parametric elementary type that can be instantiated with any solution of the set of collected constraints. We point out that the typeability of lambda terms in EAL has a practical counterpart, since it is possible to reduce any EAL-typeable lambda terms with the Lamping’s abstract algorithm obtaining a substantial increase of performances. We show how to apply the same techniques to obtain decorations of intuitionistic proofs into linear logic proofs. | |
| Handle: | http://hdl.handle.net/11390/877881 | |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| p219-coppola.pdf | Altro materiale allegato | Non pubblico | Accesso ristretto Richiedi una copia |
http://hdl.handle.net/11390/877881
Copyright © 2021