A syntactic approach to foundational proof-carrying code

DOI10.1023/B:JARS.0000021012.97318.E9MaRDI QIDQ1826465zbMATH OpenFDO

Authors Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni

Publication date 6 August 2004

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/B:JARS.0000021012.97318.E9

zbMATH Keywords

foundational proof-carrying codesyntactic soundness prooftyped assembly language

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A tutorial example of the semantic approach to foundational proof-carrying code
• Tutorial examples of the semantic approach to foundational proof-carrying code
• A tutorial example of the semantic approach to foundational proof-carrying code: Abstract
• scientific article; zbMATH DE number 2110618
• A gradual approach to a more trustworthy, yet scalable, proof-carrying code

Cited in

(18)

• Verified software units
• Type-safe code transformations in Haskell
• Imperative LF meta-programming
• Modular verification of concurrent assembly code with dynamic thread creation and termination
• Modular development of certified program verifiers with a proof assistant,
• Tutorial examples of the semantic approach to foundational proof-carrying code
• Social processes, program verification and all that
• scientific article; zbMATH DE number 2163030 (Why is no real title available?)
• Temporal logic for proof-carrying code
• scientific article; zbMATH DE number 2110618 (Why is no real title available?)
• scientific article; zbMATH DE number 6403889 (Why is no real title available?)
• A semantic model of types and machine instructions for proof-carrying code
• Towards Formal Proof Script Refactoring
• Foundational certified code in the Twelf metalogical framework
• Interfacing Hoare logic and type systems for foundational proof-carrying code
• A tutorial example of the semantic approach to foundational proof-carrying code
• A tutorial example of the semantic approach to foundational proof-carrying code: Abstract
• Automated Deduction – CADE-19

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A syntactic 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 Q1826465)