Conference Proceeding

Encoding Z-style Schemas in Type Theory



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.;

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.

Title of seriesLecture Notes in Computer Science
Number in series806
Publication date31/12/1994
Publication date online31/05/1994
Publisher URL
Place of publicationBerlin Heidelberg
ISSN of series0302-9743
ConferenceInternational Workshop TYPES'93
Conference locationNijmegen, The Netherlands

People (1)


Dr Savi Maharaj

Dr Savi Maharaj

Senior Lecturer, Computing Science