On the reification of semantic linearity

What is it about?

Linearity is a multi-faceted and ubiquitous notion in the analysis and development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between domains.

Featured Image

Why is it important?

We propose a PCF-like language imposing linear constraints on the use of variable to program only linear functions. To entail a full abstraction result, we introduce some higher-order operators related to exception handling and parallel evaluation. Finally, we present a new operational evaluation of the language that provides the base for a real implementation. It exploits the denotational linearity to provide an efficient evaluation semantics SECD-like, that avoids the use of closures.