CINECA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.
AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.
EnglishLinearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces. We introduce a language, named SlPCF*, that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF* allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler. Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. The first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. The second one is more concrete and it prunes such a space, by exploiting the linear assumptions. This can also be regarded as a base for an implementation.
| Titolo: | Linearity and PCF: a semantic insight! |
| Autori Riconosciuti: | |
| Autori: | Marco Gaboardi; Luca Paolini ; Mauro Piccolo |
| Data di pubblicazione: | 2011 |
| Abstract: | Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces. We introduce a language, named SlPCF*, that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF* allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler. Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. The first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. The second one is more concrete and it prunes such a space, by exploiting the linear assumptions. This can also be regarded as a base for an implementation. |
| Editore: | ACM |
| Titolo del libro: | ICFP '11 - Proceeding of the 16th ACM SIGPLAN international conference on Functional programming |
| Volume: | 46 |
| Fascicolo: | 9 |
| Pagina iniziale: | 372 |
| Pagina finale: | 384 |
| Nome del convegno: | ICFP '11 - 16th ACM SIGPLAN international conference on Functional programming |
| Luogo del convegno: | Tokyo, Japan |
| Anno del convegno: | September 19-21, 2011 |
| Digital Object Identifier (DOI): | 10.1145/2034773.2034822 |
| ISBN: | 9781450308656 |
| URL: | http://dl.acm.org/citation.cfm?id=2034822 |
| Parole Chiave: | linearity; coherence spaces; higher order functions and recursive theory; PCF; full abstraction |
| Appare nelle tipologie: | 04A-Conference paper in volume |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| Linearity and PCF_ a semantic insight - ACM 2011 ori.pdf | PDF EDITORIALE | Utenti riconosciuti Richiedi una copia |
http://hdl.handle.net/2318/89178
Copyright © 2020