Certifying Machine Code Safety: Shallow Versus Deep Embedding

This publication has 11 references indexed in Scilit:

• Secure mechanical verification of mutually recursive procedures
  Information and Computation, 2003
• A syntactic approach to foundational proof-carrying code
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
• A provably sound TAL for back-end optimization
  Published by Association for Computing Machinery (ACM) ,2003
• Program Extraction in Simply-Typed Higher Order Logic
  Published by Springer Nature ,2003
• Foundational proof-carrying code
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• Isabelle/HOL
  Published by Springer Nature ,2002
• Executing Higher Order Logic
  Published by Springer Nature ,2002
• A certifying compiler for Java
  Published by Association for Computing Machinery (ACM) ,2000
• A semantic model of types and machine instructions for proof-carrying code
  Published by Association for Computing Machinery (ACM) ,2000
• Proof Terms for Simply Typed Higher Order Logic
  Published by Springer Nature ,2000