Friday, April 13, 2018 - 3:30pm to 4:30pm
Location:9115 Gates Hillman Centers
Speaker:MARCELO FIORE, Professor in Mathematical Foundations of Computer Science http://www.cl.cam.ac.uk/~mpf23/
The seminal work of Moggi  identified the abstract structure of computational effects as that given by the categorical concept of a monad. Plotkin and Power  considered monads induced by algebraic theories from this computational viewpoint and developed a theory of algebraic effects. The second-order algebraic theories of Fiore et al [2, 3] are a conservative extension of the algebraic theories of universal algebra that provide algebraic foundations for simple type theories with variable binding. The theme of this talk is to consider and study them from the perspective of computational effects. Fiore and Staton  gave a computational interpretation of the second-order algebraic theory of the substitution algebras of Fiore et al  as jump effects. I will introduce more general second-order algebraic theories of inception algebras and equip them with computational interpretations as control effects. These will be justified by a CPS semantics and then related to de Groote's computational interpretation of negation elimination and the excluded middle  and to Thielecke's CPS calculus . Computational interpretations of second-order algebraic theories of the lambda calculus will also be considered. In particular, left lambda algebras will be shown to correspond to a synchronous coroutine mechanism.
Marcelo Fiore is Professor in Mathematical Foundations of Computer Science at the Department of Computer Science and Technology of the University of Cambridge. His research contributions and interests extend over the semantics of functional, concurrent, and effectful calculi; algebraic foundations for type theories and logical frameworks; and applications of category theory to computer science.
Faculty Host: Robert Harper