Visible to the public LiquidPi: Inferrable Dependent Session TypesConflict Detection Enabled

TitleLiquidPi: Inferrable Dependent Session Types
Publication TypeConference Proceedings
Year of Publication2013
AuthorsDennis Griffith, University of Illinois at Urbana-Champaign, Elsa Gunter, University of Illinois at Urbana-Champaign
Conference Name5th NASA Formal Methods Symposium NFM 2013
Date Published05/2013
PublisherSpringer-Verlag Berlin Heidelberg 2013
Conference LocationMoffett Field, CA
KeywordsCMU
Abstract

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.

Citation Keynode-30092
AttachmentTaxonomyKindSize
Griffith_LiquidPI.pdfPDF document251.9 KBDownloadPreview
AttachmentSize
bytes