Biblio

Filters: Author is Dennis Griffith, University of Illinois at Urbana-Champaign  [Clear All Filters]
2015-12-02
Dennis Griffith, University of Illinois at Urbana-Champaign, Elsa Gunter, University of Illinois at Urbana-Champaign.  2013.  LiquidPi: Inferable Dependent Session Types. 5th International NASA Formal Methods (NFM 2013) .

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.

2016-12-05
Dennis Griffith, University of Illinois at Urbana-Champaign, Elsa Gunter, University of Illinois at Urbana-Champaign.  2013.  LiquidPi: Inferrable Dependent Session Types. 5th NASA Formal Methods Symposium NFM 2013 .

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.