Jean-Marie Madiot ; Damien Pous ; Davide Sangiorgi - Modular coinduction up-to for higher-order languages via first-order transition systems

lmcs:6046 - Logical Methods in Computer Science, September 17, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:25)2021
Modular coinduction up-to for higher-order languages via first-order transition systemsArticle

Authors: Jean-Marie Madiot ; Damien Pous ; Davide Sangiorgi

    The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.


    Volume: Volume 17, Issue 3
    Published on: September 17, 2021
    Accepted on: March 11, 2021
    Submitted on: January 22, 2020
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Coinduction for Verification and Certification; Funder: European Commission; Code: 678157
    • Differential Program Semantics; Funder: European Commission; Code: 818616

    Consultation statistics

    This page has been seen 2096 times.
    This article's PDF has been downloaded 444 times.