Encoding Z-style Schemas in Type Theory

Citation

Maharaj S (1994) Encoding Z-style Schemas in Type Theory. In: Barendregt H & Nipkow T (eds.) Types for Proofs and Programs: International Workshop TYPES'93 Nijmegen, The Netherlands, May 24–28, 1993 Selected Papers. Lecture Notes in Computer Science, 806. International Workshop TYPES'93, Nijmegen, The Netherlands, 24.05.1993-28.05.1993. Berlin Heidelberg: Springer, pp. 238-262. http://link.springer.com/chapter/10.1007/3-540-58085-9_79#; https://doi.org/10.1007/3-540-58085-9_79

Abstract
A distinctive feature of the Z specification language is its Schema Calculus which allows specifications to be packaged and put together to form new specifications. We investigate methods of transporting the Schema Calculus to the type theory UTT. We first attempt a direct encoding of schemas as Σ-types. This turns out to be unsatisfactory because encoding the operations of the Schema Calculus requires the ability to perform computations on the syntax of schemas, so we develop methods in which this syntax is also represented. These methods also depend upon Σ-types but use them in an unconventional fashion. We define a notion of implementation of a schema and use the LEGO proof-checker to prove some theorems about the interaction between implementations and our encodings of the operations of the Z Schema Calculus.