A structure preserving encoding of Z in Isabelle/HOL

DOI10.1007/BFB0105411MaRDI QIDQ6567720zbMATH OpenFDO

Authors Kolyang, Thomas Santen, Burkhart Wolff

Publication date 5 July 2024

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• scientific article; zbMATH DE number 2079996
• Encoding Z-style Schemas in type theory
• Revising \(Z\). I: Logic and semantics
• Revising \(Z\). II: Logical development
• A calculus for schemas in Z

Cites work

• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• Isabelle. A generic theorem prover

Cited in

(1)

• Encoding Z-style Schemas in type theory

This page was built for publication: A structure preserving encoding of Z in Isabelle/HOL

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