Farzaneh Derakhshan ; Frank Pfenning - Circular Proofs as Session-Typed Processes: A Local Validity Condition

lmcs:5675 - Logical Methods in Computer Science, May 10, 2022, Volume 18, Issue 2 - https://doi.org/10.46298/lmcs-18(2:8)2022
Circular Proofs as Session-Typed Processes: A Local Validity ConditionArticle

Authors: Farzaneh Derakhshan ; Frank Pfenning

    Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. In this paper, we establish an extension of the latter correspondence for a fragment of substructural logic with least and greatest fixed points. We describe the computational interpretation of the resulting infinitary proof system as session-typed processes, and provide an effectively decidable local criterion to recognize mutually recursive processes corresponding to valid circular proofs as introduced by Fortier and Santocanale. We show that our algorithm imposes a stricter requirement than Fortier and Santocanale's guard condition, but is local and compositional and therefore more suitable as the basis for a programming language.


    Volume: Volume 18, Issue 2
    Published on: May 10, 2022
    Accepted on: December 18, 2021
    Submitted on: August 7, 2019
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,03B70, 97P40,F.3.1,F.3.2,F.3.3,F.4.1,D.3.1,D.1.3
    Funding:
      Source : OpenAIRE Graph
    • SHF:Small: Enriching Session Types for Practical Concurrent Programming; Funder: National Science Foundation; Code: 1718267

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1355 times.
    This article's PDF has been downloaded 908 times.