TY - GEN
T1 - LiquidPi
T2 - 5th International Symposium on NASA Formal Methods, NFM 2013
AU - Griffith, Dennis
AU - Gunter, Elsa
PY - 2013/9/9
Y1 - 2013/9/9
N2 - The Pi Calculus is a popular formalism for modeling distributed computation. Session Types extend the Pi Calculus with a static, inferable type system. Dependent Types allow for a more precise characterization of the behavior of programs, but in their full generality are not inferable. In this paper, we present LiquidPi an approach that combines the dependent type inferencing of Liquid Types with Honda's Session Types to give a more precise automatically derived description of the behavior of distributed programs. These types can be used to describe/enforce safety properties of distributed systems. We present a type system parametric over an underlying functional language with Pi Calculus connectives and give an inference algorithm for it by means of efficient external solvers and a set of dependent qualifier templates.
AB - The Pi Calculus is a popular formalism for modeling distributed computation. Session Types extend the Pi Calculus with a static, inferable type system. Dependent Types allow for a more precise characterization of the behavior of programs, but in their full generality are not inferable. In this paper, we present LiquidPi an approach that combines the dependent type inferencing of Liquid Types with Honda's Session Types to give a more precise automatically derived description of the behavior of distributed programs. These types can be used to describe/enforce safety properties of distributed systems. We present a type system parametric over an underlying functional language with Pi Calculus connectives and give an inference algorithm for it by means of efficient external solvers and a set of dependent qualifier templates.
UR - http://www.scopus.com/inward/record.url?scp=84883437596&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84883437596&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38088-4_13
DO - 10.1007/978-3-642-38088-4_13
M3 - Conference contribution
AN - SCOPUS:84883437596
SN - 9783642380877
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 185
EP - 197
BT - NASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings
Y2 - 14 May 2013 through 16 May 2013
ER -