[TYPES] Papers on Proof-Carrying Code available

[nipkow at in.tum.de]

We are pleased to announce the availability of the following papers:


"Prototyping Proof Carrying Code"

We introduce a generic framework for proof carrying code, developed
and mechanically verified in Isabelle/HOL. The framework defines and
proves sound a verification condition generator with minimal
assumptions on the underlying programming language, safety policy,
and safety logic. We demonstrate its usability for prototyping proof
carrying code systems by instantiating it to a simple assembly
language with procedures and a safety policy for arithmetic
overflow.
http://www.in.tum.de/~nipkow/pubs/tcs04.html


"Certifying Machine Code Safety: Shallow versus Deep Embedding"

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.
http://www.in.tum.de/~nipkow/pubs/tphols04.html

Comments are very welcome.

Martin Wildmoser and Tobias Nipkow