@Article{	  brucker.rittinger.ea:hol-z,
  abstract	= { We present a new proof environment for the specification
		  language Z. The basis is a semantic representation of Z in
		  a structure-preserving, shallow embedding in Isabelle/HOL.
		  On top of the embedding, new proof support for the Z schema
		  calculus and for proof structuring are developed. Thus, we
		  integrate Z into a well-known and trusted theorem prover
		  with advanced deduction technology such as higher-order
		  rewriting, tableaux-based provers and arithmetic decision
		  procedures. A further achievement of this work is the
		  integration of our embedding into a new tool-chain
		  providing a Z-oriented type checker, documentation
		  facilities and macro support for refinement proofs; as a
		  result, the gap has been closed between a logical embedding
		  proven correct and a \emph{tool} suited for applications of
		  non-trivial size.},
  author	= {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  journal	= {Journal of Universal Computer Science},
  classification= {journal},
  language	= {USenglish},
  title		= {HOL-Z 2.0: A Proof Environment for Z-Specifications},
  volume	= 9,
  year		= 2003,
  number	= 2,
  pages		= {152--172},
  month		= feb,
  issn		= {0948-6968},
  ps		= {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.ps.gz}
		  ,
  pdf		= {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.pdf}
		  ,
  copyright	= {\copyright J.UCS},
  copyrighturl	= {http://www.jucs.org/jucs_9_2/hol_z_2}
}