by Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wolff

We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a LaTeX-based front end (including the integrated type-checker ZETA), generic facilities to generate proof obligations and improved proof support for the logical embedding HOL-Z, namely for the schema-calculus and structural Z proofs.

*Keywords:*

*Categories:* ,

*Documents:* (full text as PDF file)

Please cite this article as follows:

Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wolff.
**HOL-Z 2.0: A Proof Environment for Z-Specifications**.
In *FM-TOOLS 2002*, pages 33-38, 2002. Available as Technical Report, University Augsburg, number 2002-11.

(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (

BibTeX

@InCollection{ brucker.ea:hol-z:2002,

}

abstract | = | {We present a proof environment for the specification language Z on top of Isabelle/HOL. It comprises a \LaTeX-based front end (including the integrated type-checker ZETA), generic facilities to generate proof obligations and improved proof support for the logical embedding HOL-Z, namely for the schema-calculus and structural Z proofs.}, | |

address | = | {Augsburg}, | |

author | = | {Achim D. Brucker and Stefan Friedrich and Frank Rittinger and Burkhart Wolff}, | |

booktitle | = | {FM-TOOLS 2002}, | |

editor | = | {Dominik Haneberg and Gerhard Schellhorn and Wolfgang Reif}, | |

language | = | {USenglish}, | |

month | = | {jul}, | |

note | = | {Available as Technical Report, University Augsburg, number 2002--11.}, | |

organization | = | {University Augsburg}, | |

pages | = | {33--38}, | |

= | {https://www.brucker.ch/bibliography/download/2002/brucker.ea-hol-z-2002.pdf}, | ||

title | = | {{HOL}-{Z} 2.0: {A} Proof Environment for {Z}-Specifications}, | |

url | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2002}, | |

year | = | {2002}, |