Harry Mairson
Brandeis University


I am going to talk about constructive classical logic, particularly in the guise of the duality of call-by-name and call-by-value discussed most recently by Phil Wadler at ICFP 2003. The basic idea in that paper is that call-by-value for products looks like call-by-name for sums when you exchange the role of expressions and continuations. This perspective is particularly clear when you look at continuation-passing style explanations, where the expressions and continuations are explicit. Left out of the duality is lambda abstraction (i.e., implication) and application, which are defined in terms of the other operators.
I would like to explain how these constructions appear using proofnets from linear logic. Implication depends in the above explanation on exponentials; instead, by introducing implication and coimplication (really, the "par" from linear logic) as a primitive, duality is restored in a linear way. Coimplication just describes abstraction over continuations. The result is a linear logic explanation of the Filinski symmetric lambda calculus. Also, by a direct-style transformation dual to CPS, we get new boxing (sharing) schemes for symmetric lambda calculi, including lambda-mu calculus. The programming language then has four kinds of pairing (with complementary unpairing): of two expressions (a product), two continuations (a coproduct), a continuation-expression pair (an application context), and an expression-continuation pair (a co-application context). I will conclude by talking about the problem of determining the context semantics (geometry of interaction) which distinguishes call-by-value and call-by-name.

Host:  Bob Harper
Appointments:  Norene Mears

Principles of Programming Seminars

Tuesday, March 15, 2005
3:30 p.m.
Wean Hall 4623