Bimodels and Biorthogonality for Abstract Machines

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.