Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Stephan Zdancewic

LFCS Seminar: Stephan Zdancewic

— filed under:

LolliProc: to Concurrency from Classical Linear Logic via Curry-Howard and Control

  • LFCS Seminar
When Jul 20, 2010
from 11:00 AM to 12:00 PM
Where 5.42
Add event to calendar vCal

While linear logic was originally proposed as a classical logic, its classical connectives are not obviously compatible with typical functional programming languages, and consequently the intuitionistic fragment of linear logic has seen far more use in type systems. Meanwhile, linearity has been used in many type systems for concurrent programs---e.g., session types---and is clearly quite applicable to the problems of concurrent programming, but the ways in which linearity has interacted with concurrency primitives in lambda calculi have remained somewhat ad-hoc.  In this talk we connect classical linear logic and concurrent functional programming in the language LolliProc, which provides simple primitives for concurrency that have a direct logical interpretation and that combine to provide the functionality of session types.  LolliProc features a simple process calculus ``under the hood'', but programmers never write non-atomic processes.  We illustrate LolliProc by example and prove soundness, strong normalization, and confluence results, which, among other things, guarantees freedom from deadlocks and race conditions.

This is joint work with Karl Mazurak

Document Actions