Professor Reynolds is visiting Edinburgh until the middle of next month (JCMB office 2618).

Abstract

The present-day high points of programming language design are languages such as Standard ML, and to a lesser extent Java, that are rigorously typed and provide sophisticated facilities for structuring data and modularizing programs. But these languages still have serious limitations: In combining functional and imperative programming, they introduce the problems of aliasing and interfering side effects. Moreover, by allocating all storage on a heap, they deprive the programmer of control over memory usage.

One way around these problems is to use a purely functional language with a refined type system that gives the user more control over the use of storage and, in particular, that permits the safe use of destructive updating. In this talk, we will explore such a language that is based on Benton's LNL, which combines linear logic with Moggi's computational lambda calculus.

We will formulate an operational semantics of this language, and describe its use of storage.