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 π-calculus, the λ-calculus, and a (call-by-value) λ-calculus with references.

Madiot J.-M., Pous D., Sangiorgi D. (2021). Modular coinduction up-to for higher-order languages via first-order transition systems. LOGICAL METHODS IN COMPUTER SCIENCE, 17(3), 1-39 [10.46298/LMCS-17(3:25)2021].

Modular coinduction up-to for higher-order languages via first-order transition systems

Sangiorgi D.
2021

Abstract

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 π-calculus, the λ-calculus, and a (call-by-value) λ-calculus with references.
2021
Madiot J.-M., Pous D., Sangiorgi D. (2021). Modular coinduction up-to for higher-order languages via first-order transition systems. LOGICAL METHODS IN COMPUTER SCIENCE, 17(3), 1-39 [10.46298/LMCS-17(3:25)2021].
Madiot J.-M.; Pous D.; Sangiorgi D.
File in questo prodotto:
File Dimensione Formato  
lmcsMPS_21.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione 579.72 kB
Formato Adobe PDF
579.72 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/884190
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact