Towards a trustworthy semantics-based language framework via proof generation

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

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)

Cites Work

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

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)