Vikraman Choudhury (Università di Bologna), The Duality of λ-Abstraction

Programme

Résumé

There are well-known dualities of computation in both functional and concurrent programming: input/output, expression/context, strict/lazy, sender/ receiver, forward/backwards, and several others. When viewed through an algebraic lens, these can be understood as metaphysical interpretations of rigorous mathematical dualities. 

In this talk, I will explore the duality of values and continuations (Filinski'89) through the lens of cartesian closure/co-cartesian co-closure. The main observation is that, just as higher-order functions give exponentials, higher-order continuations give co-exponentials. Using this semantic duality, I will present a λλ~ (lambda-lambda-bar or tilde) calculus, which is a call-by-value calculus extended with a classical disjunction type, that exhibits a duality of abstraction/co-abstraction. I will develop the syntax and semantics of this language, and give a computational interpretation in terms of speculative execution and backtracking. Using the language, I will show how to recover classical control operators, the computational interpretation of classical logic, and axiomatise control effects. Finally, I will show how this duality gives a nice programming idiom for control effects, that can be used in existing functional programming languages.