 |
 |
Tom Hirschowitz ; Ambroise Lafont - A categorical framework for congruence of applicative bisimilarity in higher-order languages
lmcs:7322 - Logical Methods in Computer Science, September 21, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:37)2022A categorical framework for congruence of applicative bisimilarity in
higher-order languagesArticle
Authors: Tom Hirschowitz 
; Ambroise Lafont
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 $\lambda$-calculus, and more generally all languages complying with a variant of Howe's format.
Source: arXiv.org:2103.16833
Volume: Volume 18, Issue 3
Published on: September 21, 2022
Accepted on: May 25, 2022
Submitted on: April 1, 2021
Keywords: Computer Science - Logic in Computer Science
Classifications
3 Documents citing this article
Consultation statistics
This page has been seen 2050 times.
This article's PDF has been downloaded 347 times.