Mizar's Soft Type System

In Mizar, unlike in most other proof assistants, the types are not part of the foundations of the system. Mizar is based on untyped set theory, which means that in Mizar expressions are typed but the values of those expressions are not. In this paper we present the Mizar type system as a collection of type inference rules. We will interpret Mizar types as soft types, by translating Mizar’s type judgments into sequents of untyped first order predicate logic. We will then prove that the Mizar type system is correct with respect to this translation in the sense that each derivable type judgment translates to a provable sequent.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Freek Wiedijk
• Keywords: Artificial Intelligence, Mizar Expressions, Mizar Type, Mizar’s Type Judgments, TPHOL 2007