Computational interpretations of Linear Logic

• To: types, logic, concurrency
• Subject: Computational interpretations of Linear Logic
• From: Samson Abramsky <sa@doc.imperial.ac.uk>
• Date: Tue, 6 Nov 90 18:52:38 EST
• Sender: meyer@theory.lcs.mit.edu

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

Albert,

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
appropriate.

Best wishes,

Samson

=====================================
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 
typing.

• Prev: MFCS'91
• Next: LaTeX version of article
• Index(es):
  • Main
  • Thread