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

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

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)

Cites Work

• K-Java: a complete semantics of Java
• Title not available (Why is that?)
• Results on the propositional \(\mu\)-calculus
• Matching Logic
• Title not available (Why is that?)

Cited In (2)

• Interactive matching logic proofs in Coq
• A matching logic foundation for Alk

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)