Marco Gaboardi (Università di Bologna)

Definability and Full abstraction for a Linear PCF

I present some recent results obtained in joint works with Luca Paolini and Mauro Piccolo. I first introduce SlPCF*, a linear core of PCF extended by basic primitives related to exception handling and nondeterministic evaluation, and I show that it is fully abstract for a linear model in the category of coherence spaces and linear functions. Then I show that the full abstraction result can be used to prove that the standard contextual equivalence can be handled by considering simpler observational equivalences. Finally, I show that the semantic linearity provides crucial information for the evaluation of programs by presenting a concrete evaluation machine for SlPCF that prunes efficiently the evaluation space.