Towards a trustworthy semantics-based language framework via proof generation

DOI10.1007/978-3-030-81688-9_23zbMATH Open1493.68056OpenAlexW3157277427MaRDI QIDQ832282FDOQ832282

Authors N. E. Zubov 

Publication date 25 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-81688-9_23

zbMATH Keywords

proof checkingproof generationsemantic framework

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• A self-certifying compilation framework for WebAssembly
• scientific article; zbMATH DE number 2163030
• A semantic model of types and machine instructions for proof-carrying code
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• Cogent: uniqueness types and certifying compilation

Cites work

• scientific article; zbMATH DE number 7178358 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• K-Java: a complete semantics of Java
• Matching logic
• Results on the propositional \(\mu\)-calculus

Cited in

(3)

• Interactive matching logic proofs in Coq
• A matching logic foundation for Alk
• Proof-carrying parameters in certified symbolic execution

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Maude
• Metamath
• K-Java
• KJS
• GitHub

This page was built for publication: Towards a trustworthy semantics-based language framework via proof generation

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