Corecursion and non-divergence in session-typed processes

Bernardo Toninho, Luis Caires, Frank Pfenning

Research output: Contribution to journalArticle

13 Citations (Scopus)

Abstract

Session types are widely accepted as an expressive discipline for structuring communications in concurrent and distributed systems. In order to express infinitely unbounded sessions, session typed languages often include general recursion which may introduce undesirable divergence, e.g., infinite unobservable reduction sequences. In this paper we address, by means of typing, the challenge of ensuring non-divergence in a session-typed π-calculus with general (co)recursion, while still allowing interesting infinite behaviors to be definable. Our approach builds on a Curry-Howard correspondence between our type system and linear logic extended with co-inductive types, for which our non-divergence property implies consistency. We prove type safety for our framework, implying protocol compliance and global progress of well-typed processes. We also establish, using a logical relation argument, that well-typed processes are compositionally non-divergent, that is, that no well-typed composition of processes, including those dynamically assembled via name passing, can result in divergent behavior.

Original languageEnglish
Pages (from-to)159-175
Number of pages17
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8902
DOIs
Publication statusPublished - 1 Jan 2014

Keywords

  • Logical Predicate
  • Linear Logic
  • Session Type
  • Divergent Behavior
  • Process Calculus

Fingerprint Dive into the research topics of 'Corecursion and non-divergence in session-typed processes'. Together they form a unique fingerprint.

Cite this