A syntactic approach to foundational proof-carrying code
From MaRDI portal
Publication:1826465
Recommendations
Cited in
(18)- Foundational certified code in the Twelf metalogical framework
- Theorem Proving in Higher Order Logics
- Towards Formal Proof Script Refactoring
- scientific article; zbMATH DE number 2163030 (Why is no real title available?)
- 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,
- scientific article; zbMATH DE number 2110618 (Why is no real title available?)
- scientific article; zbMATH DE number 2090286 (Why is no real title available?)
- scientific article; zbMATH DE number 6403889 (Why is no real title available?)
- Term Rewriting and Applications
- Typed Lambda Calculi and Applications
- Type-safe code transformations in Haskell
- Imperative LF meta-programming
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)
