[ICFP'26] Bimodels and Biorthogonality for Abstract Machines

Bimodels and Biorthogonality for Abstract Machines (Video, ICFP 2026) April Tune, G. A. Kavvos (University of Bristol, UK; University of Bristol, UK) Abstract: We develop a compositional semantics for abstract machines, focusing on CK/CEK machines for call-by-push-value. Taking abstract machines as the primary operational semantics, we introduce bimodels, which give denotations to both programs and stacks, and environment bimodels, which extend the construction to closures. Each has a syntactic instance, built from the machine itself, and a set-theoretic instance that serves as a denotational semantics. Using biorthogonality, we define logical relations over these models and prove fundamental lemmata that are parametric in the choice of model and observation. Different instantiations yield canonicity, adequacy, operational extensionality, internal full abstraction, and a first-order simulation theorem relating the CK and CEK machines. All results are mechanized in Agda. Article: https://doi.org/10.1145/3828686 Supplementary archive: https://doi.org/10.5281/zenodo.21490016 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) ORCID: https://orcid.org/0009-0004-9828-5194, https://orcid.org/0000-0001-7953-7975 Video Tags: abstract machines, call-by-push-value, biorthogonality, orthogonality, logical relations, mechanized metatheory, doi:10.1145/3828686, doi:10.5281/zenodo.21490016, orcid:0009-0004-9828-5194, orcid:0000-0001-7953-7975, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the ICFP 2026 conference, August 25-27, 2026, https://icfp26.sigplan.org/ Sponsored by ACM SIGPLAN.