Automating soundness proofs

DOI10.1016/J.ENTCS.2009.07.076MaRDI QIDQ2810691zbMATH OpenOpenAlexFDO

Authors Muck van Weerdenburg

Publication date 3 June 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.07.076

zbMATH Keywords

axiomatisationsoundnessstructural operational semanticstheorem proving

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Exploiting algebraic laws to improve mechanized axiomatizations
• Publication:4945209
• scientific article; zbMATH DE number 1980941
• A Sound Semantics for OCaml light
• scientific article; zbMATH DE number 2086418

Cites work

• Finite axiom systems for testing preorder and De Simone process languages
• Foundations of Software Science and Computational Structures
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 48157 (Why is no real title available?)
• scientific article; zbMATH DE number 2086418 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Process Algebra
• Structured operational semantics and bisimulation as a congruence
• The meaning of negative premises in transition system specifications
• The origins of structural operational semantics
• Untersuchungen über das logische Schliessen. I
• Using a generalisation critic to find bisimulations for coinductive proofs

Cited in

(6)

• Exploiting algebraic laws to improve mechanized axiomatizations
• Proving the validity of equations in GSOS languages using rule-matching bisimilarity
• scientific article; zbMATH DE number 1980941 (Why is no real title available?)
• scientific article; zbMATH DE number 1748586 (Why is no real title available?)
• How to make ad hoc proof automation less ad hoc
• Improving automation for higher-order proof steps

Describes a project that uses

Uses Software

• Isabelle
• PVS
• Coq
• Isabelle/HOL

This page was built for publication: Automating soundness proofs

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