Towards a trustworthy semantics-based language framework via proof generation

DOI10.1007/978-3-030-81688-9_23MaRDI QIDQ832282zbMATH OpenOpenAlexFDO

Authors N. E. Zubov

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

(4)

• Interactive matching logic proofs in Coq
• Proof-carrying parameters in certified symbolic execution
• Unification and anti-unification in applicative matching logic
• A matching logic foundation for Alk

Describes a project that uses

Uses Software

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

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)