University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > The direct approach to evaluation order

The direct approach to evaluation order

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Victor Gomes.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity