LFCS Seminar: Tuesday, 9 May - Vikraman Choudhury

Title:             Continuations and co-exponentials

Abstract:

Continuations are a mysterious but powerful concept in programming languages, that have been understood (and misunderstood) for a long time. In this talk, I will present and develop a new perspective: just as higher-order functions give you exponentials, higher-order continuations give you co-exponentials.

Using this perspective, I will show how to: (1) combine exponentials and co-exponentials in the same language without degeneracy, (2) give a computational interpretation for bi-intuitionistic logic, (3) recover classical control operators and the computational interpretation of classical logic, (4) use co-exponential combinators to do speculative execution, backtracking, and encode effect handlers, (5) add co-exponentials to a first-order programming language, with a computational interpretation. I will develop these ideas both in syntax and semantics, using a micrological study of continuations. The work is situated as part of a bigger research programme on understanding quantum foundations, using linearity, reversibility, and duality.