English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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