Savi Maharaj
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 Sigma-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 Sigma-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.