A syntactic approach to foundational proof-carrying code

DOI10.1023/B:JARS.0000021012.97318.E9zbMATH Open1069.68038MaRDI QIDQ1826465FDOQ1826465

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)

Recommendations

• Term Rewriting and Applications
• Tutorial examples of the semantic approach to foundational proof-carrying code
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 2110618
• scientific article; zbMATH DE number 2090287

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)

Cited In (18)

• Theorem Proving in Higher Order Logics
• Towards Formal Proof Script Refactoring
• Title not available (Why is that?)
• A semantic model of types and machine instructions for proof-carrying code
• Social processes, program verification and all that
• Verified software units
• Modular verification of concurrent assembly code with dynamic thread creation and termination
• Automated Deduction – CADE-19
• Tutorial examples of the semantic approach to foundational proof-carrying code
• Modular development of certified program verifiers with a proof assistant,
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• Type-safe code transformations in Haskell
• Imperative LF meta-programming
• Foundational certified code in the Twelf metalogical framework

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)