Proofs as Processes. Propositions as sessions
In this session, we explore how the propositions-as-types paradigm extends to concurrency. Upon request, the session will be hosted as a hybrid event.
Practicalities
- Location: due to high turnout, PLSL meetings now take place in the IMADA Meeting Room 4 (Ø14-605b-2).
- Time: PLSL meetings do not follow the “academic quarter” rule. The sessions start at the indicated time.
- Preparation: unless otherwise specified, reading the assigned material in advance is required to join PLSL sessions proficuously.
Material
The material to be read before the meeting is:
- Samson Abramsky, Proofs as processes, Theoretical Computer Science, Volume 135, Issue 1, 1994, Pages 5-9, ISSN 0304-3975
- sections 1-2 from Philip Wadler, Propositions as sessions, Journal of Functional Programming, Volume 2014, Issue 24(2–3), 2014, Pages 384–418, doi:10.1017/S095679681400001X
Abstract (Propositions as sessions)
Continuing a line of work by Abramsky (1994), Bellin and Scott (1994), and Caires and Pfenning (2010), among others, this paper presents CP, a calculus, in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), Honda et al. (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and 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 yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.
Before joining
Please make sure to be aware of the PLSL format before joining.