Linear Observations & Computational Effects

1. The 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.
2. A novel notion of proof net, which provides an efficient decision procedure for an important type theory ("additive linear logic with units", which arises both as a fragment of EEC and as a fragment of Girard's linear logic) was developed. Obtaining a canonical proof-net treatment of "additive units" was previously an open problem in linear logic.
3. 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).