Harry Mairson
Brandeis University
Abstract:
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