pdfreaders.org

HOL-Z 2.0: A Proof Environment for Z-Specifications

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

Cover for brucker.ea:hol-z:2002.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)

QR Code for brucker.ea:hol-z:2002.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) (Share article on LinkedIn. Share article on CiteULike. )

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},
pdf = {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},
}