LiquidPi: Inferrable dependent session types

Dennis Griffith, Elsa L. Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 5th International Symposium, NFM 2013, Proceedings
Pages185-197
Number of pages13
DOIs
StatePublished - 2013
Event5th International Symposium on NASA Formal Methods, NFM 2013 - Moffett Field, CA, United States
Duration: May 14 2013May 16 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7871 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other5th International Symposium on NASA Formal Methods, NFM 2013
Country/TerritoryUnited States
CityMoffett Field, CA
Period5/14/135/16/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'LiquidPi: Inferrable dependent session types'. Together they form a unique fingerprint.

Cite this