The direct approach to evaluation order

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

• Guillaume Munch-Maccagnoni, INRIA
• Tuesday 19 June 2018, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.