Abstract

This talk is about the theory of computation with evaluation order, for instance in the presence of effects and/or resources. I will revisit the relationship between two lines of work in this context: focusing (from the proof search paradigm) and call-by-push-value (from the monadic semantics paradigm). I present a self-contained approach which contains, connects, and generalizes their principal concepts and results. Both paradigms gain new questions, and their relationship is explained, as they become unified. The result is a Curry-Howard correspondence in the original sense of Lambek: an internal language for call-by-push-value that comes with a guarantee of fitness for a purpose, here for instance we obtain for free a solution to the word problem. As for the old formalisms, some are decomposed (focusing), others are made redundant (call-by-push-value-style syntaxes).

The approach is built on top of an old theorem due to Führmann relating “direct-style” deductive systems to algebraic models. Until recently this result was more of a curiosity, but it has resurfaced in several works. I propose to make it a mediating principle between logic, computation and algebra, so the talk will focus on explaining this point of view.