Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2103786.2103788 | TLDI |
Keywords | Field | DocType |
dependent type,type system,towards concurrent type theory,resulting system,type preservation,functional term,concurrent computational interpretation,functional type theory,session type,dependent concurrent type theory,curry-howard isomorphism,π calculus,type theory,linear logic,dependent types,satisfiability | Intuitionistic type theory,Computer science,π-calculus,Type theory,Theoretical computer science,Mathematical proof,Isomorphism,Sequent,Linear logic,Dependent type | Conference |
Citations | PageRank | References |
7 | 0.51 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Luís Caires | 1 | 1037 | 63.30 |
| Frank Pfenning | 2 | 3376 | 265.34 |
| Bernardo Toninho | 3 | 201 | 14.31 |