CSM-344 - Two Semantic Embeddings of Z Schemas in Isabelle/HOL
Norbert Völker · Open Access at Essex (University of Essex) · 2001
This report investigates two semantic embeddings of Z schemas in Isabelle/HOL. The first represents Z values as elements of a type class with polymorphic type constructors and overloaded operators. In contrast, the second embedding uses a Z universe: all Z values are represented as elements of a single monomorphic HOL type.