Certifying Machine Code Safety: Shallow versus Deep Embedding

Martin Wildmoser, Tobias Nipkow

We formalise a simple assembly language with procedures and a safety policy for arithmetic overflow in Isabelle/HOL. To verify individual programs we use a safety logic. Such a logic can be realised in Isabelle/HOL either as shallow or deep embedding. In a shallow embedding logical formulas are written as HOL predicates, whereas a deep embedding models formulas as a datatype. This paper presents and discusses both variants pointing out their specific strengths and weaknesses.

pdf (c) Springer Verlag


author={Martin Wildmoser and Tobias Nipkow},
title={Certifying Machine Code Safety: Shallow versus Deep Embedding},
booktitle={Theorem Proving in Higher Order Logics (TPHOLs 2004)},
editor={K. Slind and A. Bunker and G. Gopalakrishnan},