It is known that abstract machines can be derived from calculi with explicit substitutions through well-understood program transformations. Formalising them in dependently-typed programming languages allows for obtaining machines proven to be correct. This work introduces the Agda formalisation of an executable and terminating CEK machine, obtained from simply typed call-by-value λp̂-calculus. The novel contributions have been the successful extension of Swierstra’s previous research on the Krivine machine to a broader case, as well as providing elegant Tait-style proof of Strong Normalisation of call-by-value λp̂-calculus.

Graduate of BSc Computer Science at the University of Southampton, interested in Programming Language Theory and Verification. From September, I will be a PhD student at UCL supervised by Prof. Alexandra Silva. Currently interning at Goldman Sachs in London and previously worked at Software and Large Scale Systems Research Group at ARM in Cambridge.