文章基本信息

标题：A CATEGORICAL FRAMEWORK FOR CONGRUENCE OF APPLICATIVE BISIMILARITY IN HIGHER-ORDER LANGUAGES
本地全文：下载
作者：Tom Hirschowitz ; Ambroise Lafont.
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2022
卷号：18
期号：3
页码：1-72
DOI：10.46298/lmcs-18(3:37)2022
语种：English
出版社：Technical University of Braunschweig
摘要：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.
关键词：Programming languages;categorical semantics;operational semantics;Howe’s method.