Bisimulations up-to: Beyond first-order transition systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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 the notion of compatible function for fixed-point theory. 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.

Original languageEnglish
Title of host publicationConcurrency Theory - 25th International Conference, CONCUR 2014, Proceedings
PublisherSpringer Verlag
Pages93-108
Number of pages16
ISBN (Print)9783662445839
DOIs
Publication statusPublished - 1 Jan 2014
Externally publishedYes
Event25th International Conference on Concurrency Theory, CONCUR 2014 - Rome, Italy
Duration: 2 Sept 20145 Sept 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8704 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Concurrency Theory, CONCUR 2014
Country/TerritoryItaly
CityRome
Period2/09/145/09/14

Fingerprint

Dive into the research topics of 'Bisimulations up-to: Beyond first-order transition systems'. Together they form a unique fingerprint.

Cite this