Formalising the SECD machine with nominal Isabelle
Gergely Buday · 2015
Charguéraud [6] lists three ways of verifying functional programs: first is to define Hoare triples, second is to define programs directly in a theorem prover, that is shallow embedding and the third is to define the semantics of the language in the logic of a theorem prover, use this definition to write programs and then prove correctness of these, this is called deep embedding.