Coalgebras and Higher-Order Computation: a GoI Approach

Abstract

Girard's geometry of interaction (GoI) can be seen---in one practical
aspect of it---as a compositional compilation method from functional
programs to sequential machines. There tokens move around and express
interactions between (parts of) programs. Intrigued by the combination
of abstract structures and concrete dynamics in GoI, our line of work
has aimed at exploiting, in GoI, results from the theory of
coalgebra---a categorical abstraction of state-based transition
systems that has found its use principally in concurrency theory. Such
reinforced connection between higher-order computation and state-based
dynamics is made possible thanks to an elegant categorical
axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced
monoidal categories are identified to be the essential structure
behind. In the talk I shall lay out these basic ideas, together with
some of our results on: GoI semantics for a quantum programming
language; and our ``memoryful'' extension of GoI with algebraic
effects.
The talk is based on my joint work with my colleague Naohiko Hoshino (RIMS, Kyoto Univer- sity) and my (former) students Koko Muroya (University of Birmingham) and Toshiki Kataoka
(University of Tokyo), to whom I owe special thanks.