Summary of EPSRC Research Grant EP/F042043/1

1st April 2008 - 30th April 2011.

This project developed a canonical calculus, the *Enriched Effect
Calculus (EEC)*, for modelling the *linear usage of effects*, whereby
standard programming idioms ensure that the individuality of effects
is respected. As a major case study, the pervasive phenomenon of the
linear usage of continuations, under different evaluation strategies
(call-by-value, call-by-name), was explained as arising from a single
subsuming continuation-passing-style translation of EEC into itself.
As a start towards analysing the problem of understanding
the equality relation between terms of EEC,
a novel notion of *proof net*, which provides an efficient
decision procedure for an interesting fragment of the calculus (*additive
linear logic with units*), was developed.

A further contribution of the project was to develop a general mathematical theory explaining the nature of behavioural equivalence for programs with effects. Whereas previously such equivalences have been axiomatized as basic (via equational presentations of algebraic theories of effects), we instead implement them as observational equivalences, so programs are only distinguished if their observable behaviour differs. The novelty here is to build a basic notion of observation directly into the mathematical model, using it to determine all the other components usually required to model effects. This provides a systematic basis for obtaining generic proofs of operational properties of programs that are valid uniformly across the many different kinds of computational effects.

A last contribution is to the development of logics and proof methods
for reasoning about the combination of nondeterministic and
probabilistic effects exhibited by probabilistic concurrent
processes. The project has developed an extension of a standard
fixed-point logic (*probabilistic mu-calculus*) with a new *independent
product* operation (modelling independent probabilistic events).
This logic generalises other established logics
for probabilistic systems (for example, *qualitative PCTL*), but has
the benefit of possessing a conceptually straightforward semantics
based on two-player stochastic games.

The research of this project resulted in 6 refereed conference papers, 6 completed journal papers (3 accepted, 3 under review) plus 2 in preparation, five keynote talks at conferences and workshops, and two conference-paper prizes (the ETAPS 2011 Best Student Paper Award to Mio, and the Kleene Award for Best Student Paper at LICS 2011 to Heijltjes).

Dr. Jeff Egger (Postdoctoral Research Assistant)

From May 2011, Jeff held a Visiting Fellowship at Macquarie University, Australia

Mr. Willem Heijltjes (PhD Student)

PhD submission August 2011

From October 2011, Willem will be a Postdoctoral Research Assistant
at Equipe Parsifal, LIX and INRIA Saclay, Ecole Polytechnique, France

Mr. Matteo Mio (PhD Student)

PhD submission October 2011

From November 2011, Matteo will take up a 2-year ERCIM Postdoctoral
Fellowship to spend 1 year at Equipe Comete, LIX and INRIA Saclay, Ecole
Polytechnique, France, then 1 year at CWI, Amsterdam

Dr. Matija Pretnar (PhD Student)

PhD Awarded June 2010.

Since September 2009 Matija has been employed as a teaching assistant at
the Faculty of Mathematics and Physics, University of Ljubljana, Slovenia

**Enriching an effect calculus with linear types** (pdf)

Jeff Egger, Rasmus Møgelberg and Alex Simpson

In Proceedings of *Computer Science Logic (CSL) 2009*

Springer LNCS 5771, pp. 240-254, 2009.

**Linearly-used continuations in the enriched effect calculus**
(pdf)

Jeff Egger, Rasmus Møgelberg and Alex Simpson

In Proceedings of *Foundations of Software Science and Computation Structures (FoSSaCS) 2010*

Springer LNCS 6014, pp. 18-32, 2010.

**A generic operational metatheory for algebraic effects**
(pdf)

Patricia Johann, Alex Simpson and Janis Voigtländer

In Proceedings of *Logic in Computer Science (LICS) 2010*, pp. 209-218.

**The equivalence of
game and denotational semantics
for the probabilistic mu-calculus**
(pdf)

Matteo Mio

In Proceedings of *Fixed Points in Computer Science (FiCS) 2010*, pp. 53-59.

**Probabilistic modal mu-calculus with independent product**
(pdf)

Matteo Mio

In Proceedings of *Foundations of Software Science and Computation Structures (FoSSaCS) 2011*

Springer LNCS 6604, pp. 290-304, 2011.

ETAPS 2011 Best Student Paper Award

**Proof nets for additive linear logic with units**
(pdf)

Willem Heijltjes

In Proceedings of *Logic in Computer Science (LICS) 2011*, pp. 207-216.

Kleene Award for Best Student Paper at LICS 2011

**Classical Proof Forestry**
(pdf)

Willem Heijltjes

*Annals of Pure and Applied Logic* 161 (11), pp. 1346-1366, 2010.

**On involutive monoidal categories**
(pdf)

Jeff Egger

*Theory and Applications of Categories* 25 (14), pp. 368-393, 2011.

**On cyclic star-autonomous categories**
(pdf)

Jeff Egger and Micah McCurdy

To appear in *Journal of Pure and Applied Algebra*

Special issue for selected papers from *Category Theory 2010*

**On the equivalence of
game and denotational semantics
for the probabilistic mu-calculus**
(pdf)

Matteo Mio

Invited submission to special issue of *Theoretical Informatics and Applications* for selected papers from FiCS 2010.

Submitted December 2010.

**Linear-use CPS translations in the enriched effect calculus**
(pdf)

Jeff Egger, Rasmus Møgelberg and Alex Simpson

Invited submission to special issue of *Logical Methods in Computer Science* for selected papers from FoSSaCS 2010.

Submitted January 2011.

**The Enriched Effect Calculus: Syntax and Semantics**
(pdf)

Jeff Egger, Rasmus Møgelberg and Alex Simpson

Invited submission to special issue of *Journal of Logic and Computation* for selected papers from LINEARITY 2009.

Submitted June 2011.

**Categorical Models for the Enriched Effect Calculus**

Jeff Egger, Rasmus Møgelberg and Alex Simpson

**A generic operational metatheory for algebraic effects**

Patricia Johann, Alex Simpson and Janis Voigtländer

Journal version of LICS 2010 paper.