Where: FCUL, room C6.3.27

Abstract: The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lambda-calculus, we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the proof-term language of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation, reconstructs the original CPS-translation. Going back to direct style, the “essence” of the VFS-translation is that it reveals a dilemma in the syntax of Moggi’s calculus, concerning how to expand the application constructor, and giving rise to two sublanguage of ANF: one is a reflection of LJQ, the other is a reflection of a natural deduction with generalized applications.

Short Bio: The speaker has a Bachelor’s Degree in Mathematics and Computer Science (Universidade do MInho, 1993), a Master’s Degree in Applied Mathematics (Instituto Superior Técnico, 1997), and a PhD Degree from the Faculty of Science and Engineering of the University of Edinburgh (2002). He is a member of the Department of Mathematics, University of MInho, where he was the director of the Master’s Degree in Mathematics and Computation (2007-2016). He is a member of the Centre of Mathematics, University of MInho, of which he was vice-director (2020-2022). He served in the Steering Committee of the TYPES Conference (2017-2020). He co-organized two editions of the conference Days in Logic (2014, 2022). He is a founder member of the Portuguese Society of Logic. His research interests are in the areas of proof theory, type theory, and lambda-calculus.