Algebraic Theories and Control Effects

Marcelo Fiore

(University of Cambridge)

I will start by analysing the second-order equational theory of substitution algebras [1] as a computational effect, and therein give an interpretation of substituting as a code-jumping mechanism [2]. Subsequently, I will introduce more general second-order equational theories of inception algebras, considering examples both from logic and computation to which I will give computational interpretations as further programming control effects.

[1] M Fiore, G Plotkin and D Turi (1999). Abstract syntax and variable binding.

[2] M Fiore and S Staton (2014). Substitution, jumps, and algebraic effects.

Thursday 29th May 2014, 14:00
Robert Recorde Room
Department of Computer Science