Tutorial examples of the semantic approach to foundational proof-carrying code

MaRDI QIDQ3593496zbMATH OpenFDO

Authors Amy P. Felty

Publication date 20 July 2007

zbMATH Keywords

Hoare-style reasoning

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• A syntactic approach to foundational proof-carrying code
• scientific article; zbMATH DE number 2090287
• scientific article; zbMATH DE number 1962754

Cited in

(11)

• A syntactic approach to foundational proof-carrying code
• Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
• scientific article; zbMATH DE number 1614684 (Why is no real title available?)
• scientific article; zbMATH DE number 1962754 (Why is no real title available?)
• From programming-by-example to proving-by-example
• A semantic model of types and machine instructions for proof-carrying code
• Foundational certified code in the Twelf metalogical framework
• Certified assembly programming with embedded code pointers
• Theorem Proving in Higher Order Logics
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications

This page was built for publication: Tutorial examples of the semantic approach to foundational proof-carrying code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3593496)