A categorical framework for congruence of applicative bisimilarity in higher-order languages
Logic in Computer Science
2023-06-22 v5
Abstract
Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name, call-by-value, and call-by-name non-deterministic -calculus, and more generally all languages complying with a variant of Howe's format.
Keywords
Cite
@article{arxiv.2103.16833,
title = {A categorical framework for congruence of applicative bisimilarity in higher-order languages},
author = {Tom Hirschowitz and Ambroise Lafont},
journal= {arXiv preprint arXiv:2103.16833},
year = {2023}
}