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

zbMATH Open1121.68029MaRDI QIDQ3593496FDOQ3593496

Authors: Amy P. Felty 

Publication date: 20 July 2007

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

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)

Cited In (11)

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

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)