Anja Petković: Equality Checking for Dependent Type Theories: Theoretical foundations

Abstract: Proof assistants based on type theories rely on equality checking algorithms to prove judgemental equalities and provide computation-by-normalization engines. I will present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules. I will discuss the properties of such rules that ensure soundness of the equality checking algorithm and introduce a type-theoretic concept of object-invertible rules. I will also comment on a sufficient syntactic criteria for recognizing such rules, to get a simple pattern-matching algorithm for applying them. If time permits, we will see how the algorithm is used in the Andromeda 2 proof assistant.

This is joint work with Andrej Bauer.