2023/03/21 by Tom Hirschowitz, Hirschowitz, Tom, Ambroise Lafont +1
Computer Science · #Advanced Algebra and Logic #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2303.11679
openalex publication_date 2023/03/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We prove a general congruence result for bisimilarity in higher-order languages, which generalises previous work to languages specified by a labelled transition system in which programs may occur as labels, and which may rely on operations on terms other than capture-avoiding substitution. This is typically the case for PCF, λ-calculus with delimited continuations, and early-style bisimilarity in higher-order process calculi.