Compiling effectful terms to transducers: prototype implementation of memoryful Geometry

In this preliminary report for LOLA 2014, we present a prototype implementation of the memoryful GoI framework in [Hoshino, Muroya and Hasuo, CSL-LICS 2014] that translates lambda terms with algebraic effects to transducers. Those transducers can be thought of as “proof nets with memories ” and are constructed in a compositional manner by means of coalgebraic component calculi. The transducers thus obtained can be simulated in our tool, too, helping us to scrutinize the step-by-step interactions that take place in higher-order effectful computation. Geometry of Interaction (GoI) Girard’s Geometry of Interaction (GoI) [6] is interaction based semantics of linear logic proofs and, via suitable translations, of functional programs in general. The mathematical cleanness of GoI has successfully identified various essential structures in computation; moreover its use as a compila-tion technique from programs to state machines—“GoI implemen