On the Structure of Mizar Types
Grzegorz Bancerek · Electronic Notes in Theoretical Computer Science · 2003
The aim of this paper is to develop a formal theory of Mizar types. The examples are extracted from Mizar Mathematical Library (MML), some of them are simplified or presented in a bit different way. The presented theory is an approach to the structure of Mizar types as a sup-semilattice with widening (subtyping) relation as the order. It is an abstraction from the existing implementation of the Mizar verifier by Andrzej Trybulec and Czesław Byliński. The theory describes the structure of types of the base fragment of Mizar language.