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. Copyright © 2011 ACM.
Linearity and PCF: A semantic insight!
Gaboardi M.Membro del Collaboration Group
;Paolini L.
;
2011-01-01
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. Copyright © 2011 ACM.
| File | Dimensione | Formato | |
|---|---|---|---|
|
Linearity and PCF_ a semantic insight - ACM 2011 ori.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
559.83 kB
Formato
Adobe PDF
|
559.83 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.
