Modular coinduction up-to for higher-order languages via first-order transition systems
| Autor: | Damien Pous, Davide Sangiorgi, Jean-Marie Madiot |
|---|---|
| Přispěvatelé: | Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Preuves et Langages (PLUME), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Plume, ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), European Project: 678157,H2020,ERC-2015-STG,CoVeCe(2016), European Project: 818616,H2020-EU.1.1. - EXCELLENT SCIENCE - European Research Council (ERC),DIAPASoN(2019), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), European Project: 818616,DIAPASoN, Madiot J.-M., Pous D., Sangiorgi D. |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Bisimulation
FOS: Computer and information sciences Computer Science - Logic in Computer Science Computer Science - Programming Languages General Computer Science Programming language business.industry Computer science Transition (fiction) [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] bisimulation λ-calculus process calculi up-to techniques labelled transition systems Modular design Reuse computer.software_genre First order Theoretical Computer Science Logic in Computer Science (cs.LO) Compatibility (mechanics) Higher order languages business computer Programming Languages (cs.PL) |
| Zdroj: | Logical Methods in Computer Science Logical Methods in Computer Science, 2021, Volume 17, Issue 3, ⟨10.46298/lmcs-17(3:25)2021⟩ Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, Volume 17, Issue 3, ⟨10.46298/lmcs-17(3:25)2021⟩ |
| ISSN: | 1860-5974 |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|