Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs
Logic in Computer Science
2021-03-09 v2 Programming Languages
Abstract
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes under an asynchronous communication semantics. As far as we are aware, this is the first proof of this property.
Cite
@article{arxiv.2001.05132,
title = {Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs},
author = {Farzaneh Derakhshan and Frank Pfenning},
journal= {arXiv preprint arXiv:2001.05132},
year = {2021}
}