Name
Abstract | ||
|---|---|---|
Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. We present a pi calculus with assume and assert operations, typed using a session discipline that incorporates refinement formulae written in a fragment of Multiplicative Linear Logic. Our original combination of session and refinement types, together with the well established benefits of linearity, allows very fine-grained specifications of communication protocols in which refinement formulae are treated as logical resources rather than persistent truths. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.4204/EPTCS.101.4 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
Field | DocType | Issue |
Multiplicative function,Refinement calculus,Pi calculus,Computer science,Linearity,Theoretical computer science,Concurrent computing,Linear logic,Predicate (grammar),Communications protocol | Journal | 101 |
ISSN | Citations | PageRank |
2075-2180 | 4 | 0.42 |
References | Authors | |
10 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pedro Baltazar | 1 | 22 | 3.35 |
| Dimitris Mostrous | 2 | 130 | 6.37 |
| Vasco Thudichum Vasconcelos | 3 | 859 | 50.71 |