Computer Laboratory

Publications, Reports, Talks, etc.

We present a general theory of Gifford-style type-and-effect annotations, where effect annotations are sets of effects, such as memory accesses or exceptions. Our theory accounts for effect-dependent program transformations for functional-imperative languages, as used in optimising compilers. Using our theory, we validate and generalise many existing optimisations and add new ones. Our general theory also suggests a classification of these optimisations into three classes, structural, local, and global. We also give modularly-checkable necessary and sufficient conditions for validating the optimisations.

Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand. The universal algebraic perspective gives an elementary and concrete view on the monadic concepts. The key observation is that annotation effects can be identified with the algebraic operation symbols. We describe how the universal algebraic approach gives particularly simple characterisations of the optimisations: structural optimisations always hold; local ones depend on the effect theory at hand; and global ones depend on the global nature of that theory, such as idempotency or absorption laws. Time permitting, we outline how the theory generalises to more sophisticated notions of universal algebra via enriched Lawvere theories and factorisation systems.

Joint work with Gordon Plotkin.

A brief introduction to programming language semantics. We will covere key aspects of the operational and denotational approaches, including type soundness, denotational soundness, adequacy. I will present a logical relations proof, and show how category theory allows to restructure it as a model in a suitable category of predicates.

We present operational semantics for effect handlers. Introduced by Plotkin and Pretnar, effect handlers form the basis of Bauer and Pretnar’s Eff programming language. Our talk outlines three contributions. * We propose the first small-step structural operational semantics for a higher-order programming language with effect handlers, and a sound type and effect system. * We exhibit two alternative effect handler implementation techniques using free monads, and using composable continuations.

  • We show that Filinski’s monadic reflection is subsumed by effect handlers.

We present a small-step operational semantics for a simplified Call-by-Push-Value variant of Bauer and Pretnar’s Eff programming language. Eff incorporates functional and imperative features by adapting Plotkin and Pretnar’s effect handlers as a programming paradigm.

This is preliminary work with Sam Lindley and Nicolas Oury.

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated imperative and functional language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalizing many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity). Joint work with Gordon Plotkin, to appear in POPL’12.

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated version of Levy’s Call-by-Push-Value language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).

Joint work with Gordon Plotkin.

" We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated version of Levy’s Call-by-Push-Value language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).“”

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols. We develop an annotated imperative and functional language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).

Joint work with Gordon Plotkin, to appear in POPL’12.

Defining the formal meaning of programming languages has been investigated for nearly half a century. The foundational questions in the field have impact on programming language theoreticians, designers and implementors. In this quasi-historical session, we’ll review the goals underlining semantics, and how operational and denotational methods have been devised to investigate them. The review will be followed by a short discussion about the current state of the theory, tools and methodologies available. Was it a big waste of time?

“We propose a probabilistic interpretation of a class of reversible communicating processes. The rate of forward and backward computing steps, instead of being given explicitly, is derived from a set of formal energy parameters. This is similar to the Metropolis-Hastings algorithm. We find a lower bound on energy costs which guarantees that a process converges to a probabilistic equilibrium state (a grand canonical ensemble in statistical physics terms). This implies that such processes hit a success state in finite average time, if there is one.”"

We propose a semantic foundation for optimisations based on type and effect analysis. We present a multiple-effect CBPV-based calculus whose denotational semantics is based on an effect-indexed structure of adjunctions. When the underlying set of effects is specified by an algebraic theory, we take effects to be given by sets of operations. The required adjunction structure can then be obtained via a uniform process of conservative restriction of the theory. The calculus and its semantics is then extended by a straightforward generalisation of Pretnar and Plotkin’s effect handlers to arbitrary, non-algebraic, inter-effect handlers.

The modular composition of effects then boils down to ex- tension conservativeness, and we show that some common ways to compose arbitrary effects by sums and tensors are indeed conservative. In particular we obtain conservative extension results for both the sum of a monad and a free monad, and also for a unification of three common instances of the tensor of theories that is obtained using monoid actions. This unification includes the usual reader, state and writer monads and monad transformers.

We use our calculus and its semantics to provide general effect- dependent optimisations. We exemplify the machinery developed by deriving a language with state, IO and exceptions, and their handlers. Many of the already known effect-dependent optimisations are then particular cases of our general ones. We have thus demonstrated the possibility of a general theory of effect optimisations based on the algebraic theory of effects.

Joint work with Gordon Plotkin.

There is a conceptual connection between the State, Reader and Writer monads. However, the State and Reader monads only require a type, whereas the Writer monad requires a monoid. I will introduce and use Plotkin’s and Power’s algebraic theory of effects to formalise this connection using the notions of monoid actions and conservative restriction. This work results in a generalised notion of the State and Reader monads and monad transformers for an arbitrary monoid action. This is joint work with Gordon Plotkin.

At the end of last year, a prominent Category Theorist revealed a well kept secret on the categories mailing list. I will present a brief overview of the various threads that erupted from this revelation, and how they are relevant to Your Research (TM).