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

Robert Recorde Room

Department of Computer Science