Linear Observations and Computational Effects

Summary of EPSRC Research Grant EP/F042043/1
1st April 2008 - 30th April 2011.

Project summary

Computational effects is a collective term for the imperative aspects of computation, such as modifying state, raising exceptions, jumping, input/output, nondeterminism, etc., which together comprise a program's behaviour during execution. Typically, each occurrence of an effect is an individual event with its own identity. This separateness of distinct events is most naturally modelled using a special kind of "linear" logic which enforces the individuality of different occurrences.

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).

People

Prof. Alex Simpson (Principal Investigator)

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

Publications

Conference papers

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

Journal papers

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

Journal papers under review

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.

Journal papers in preparation

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.