Towards a trustworthy semantics-based language framework via proof generation

DOI10.1007/978-3-030-81688-9_23zbMath1493.68056MaRDI QIDQ832282

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 checking; proof generation; semantic framework

Mathematics Subject Classification ID

68N15: Theory of programming languages

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

Uses Software

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