Computational interpretations of Linear Logic

Date: Tue, 30 Oct 90 18:17:58 GMT


I've just completed a paper on this topic. Please put the abstract on any
of the lists (types, concurrency etc.) for which you think it would be

Best wishes,


Computational Interpretations of Linear Logic

Samson Abramsky

Imperial College

We study Girard's Linear Logic from the point of view of giving a concrete
computational interpretation of the logic, based on the Curry-Howard
isomorphism. In the case of Intuitionistic Linear Logic, this leads to
a refinement of the lambda calculus, giving finer control over order
of evaluation and storage allocation, while maintaining the logical content
of programs as proofs, and computation as cut-elimination. In the classical
case, it leads to a concurrent process paradigm with an operational
semantics in the style of Berry and Boudol's Chemical Abstract machine.
This opens up a promising new approach to the parallel implementation of
functional programming languages; and offers the prospect
of typed concurrent programming in which correctness is guaranteed by the