Monday, November 16, Volen 101, 3-5 p.m.
(This is the second 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.)
The previous seminar in this series introduced Linear Logic, a ``resource conscious'' logic. We now consider in further detail its use as a tool for programming language implementation.
In particular, the idea of a box from proofnets for Linear Logic provides a consistent way of representing shared values. For instance, we can put a function in a box so that it can be passed around as a value, and be used more than once.
In considering the questions of what boxes to duplicate, and when to do so, we are lead to a description of different reduction strategies, and ultimately to optimal strategies that do no ``extra work.'' We show that such a strategy can be implemented in several ways, corresponding to different encodings of Intuitionistic Logic into Linear Logic. These implementations provide a logical explanation of the familiar call-by-name (CBN) and call-by-value (CBV) paradigms for procedure calling. In translating an ``ordinary type'' t into a ``linear type'' [t], in the call-by-name translation we have [a->b] = ![a] -o [b], while in the call-by-value translation we have [a->b] = !([a] -o [b]).
Finally, we begin a discussion of how this perspective can be extended to languages with first-class continuations, so that functions can also transform control contexts for programs.