Towards concurrent type theory

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)

Abstract

We review progress in a recent line of research that provides a concurrent computational interpretation of (intuitionistic) linear logic. Propositions are interpreted as session types, sequent proofs as processes in the pi-calculus, cut reductions as process reductions, and vice versa. The strong proof-theoretic foundation of this type system provides immediate opportunities for uniform generalization, specifically, to embed terms from a functional type theory. The resulting system satisfies the properties of type preservation, progress, and termination, as expected from a language derived via a Curry-Howard isomorphism. While very expressive, the language is strictly stratified so that dependent types for functional terms can be enforced during communication, but neither processes nor channels can appear in functional terms. We briefly speculate on how this limitation might be overcome to arrive at a fully dependent concurrent type theory.
Original languageUnknown
Title of host publicationProceedings of the 8th ACM SIGPLAN workshop on Types in Language Design and Implementation (TLDI`12)
Pages1-12
DOIs
Publication statusPublished - 1 Jan 2012
EventTLDI`12 - 8th ACM SIGPLAN workshop on Types in Language Design and Implementation -
Duration: 1 Jan 2012 → …

Conference

ConferenceTLDI`12 - 8th ACM SIGPLAN workshop on Types in Language Design and Implementation
Period1/01/12 → …

Cite this