Monday, November 2, Volen 101, 3-5 p.m.
(This is the first of a bimonthly research seminar at Brandeis on programming language theory and implementation. It is being run jointly with the Church group at Boston University---on alternate weeks we will meet at BU.)
I am going to give a general talk about linear logic, a new logic of resources proposed in 1987 by Jean-Yves Girard. Among other things, linear logic challenges the persistence of truth through time: if A => B and A are true, and we deduce B, is A still true? (Let A be ``I have $1'' and B be ``I buy some coffee.'') Linear logic pays particular attention to the duplication and erasure of hypotheses.
It turns out that programming language implementation must attend to similar issues. Implementation pragmatics must say when values are copied or thrown away, or when values can be shared without copying them. These questions become even more complicated in languages where the control (i.e., the continuation) can be manipulated by the program (jumps, call/cc, etc.).
I hope to give listeners a grasp of what linear logic is like, and why someone interested in programming language design and implementation might want to know about it.
Reading: Jean-Yves Girard, Linear logic: its Syntax and Semantics