Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Phil Wadler

LFCS Seminar: Phil Wadler

— filed under:

Propositions as Sessions

  • LFCS Seminar
When May 03, 2012
from 02:00 PM to 03:00 PM
Where IF 4.31-33
Add event to calendar vCal

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this talk presents CP, a calculus in which propositions of classical linear logic correspond to session types.  Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this talk presents GV, a linear functional language with session types, and presents a translation from GV into CP.  The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.

Document Actions