Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329229 | Electronic Notes in Theoretical Computer Science | 2005 | 20 Pages |
Abstract
This paper studies the typechecking problem for Iris, a typed Ï-calculus that combines session types and correspondence assertions. We define a typechecking algorithm and prove that it is sound and complete with respect to the typing rules. Furthermore, we show that the typing system satisfies the minimum effects property. Although session types have been extensively studied in the past few years, to our knowledge this is the first proof of decidability of typechecking for a type system with session types.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Eduardo Bonelli, Adriana Compagnoni, Elsa Gunter,