LFCS Seminar: Stephan Zdancewic
LolliProc: to Concurrency from Classical Linear Logic via CurryHoward and Control
What 


When 
Jul 20, 2010 from 11:00 AM to 12:00 PM 
Where  5.42 
Add event to calendar 
vCal iCal 
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 programse.g., session typesand 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 adhoc. 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 nonatomic 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