Anja Petković: Equality checking for Finitary type theories
Source: Mathematics and theoretical computing seminar
To attend follow this Zoom link.
Abstract: Equality checking algorithms are essential components of proof assistants based on type theories, since they free users from the burden of proving judgemental equalities, and provide computation-by-normalization engines. Indeed, the type theories found in the most popular proof assistants are designed to provide such algorithms.
However, in a proof assistant that supports arbitrary user-definable theories, such as Andromeda 2, there may not be an equality checking algorithm available in general.
I will discuss the design of a user-extensible judgemental equality checking algorithm for finitary type theories that supports computation rules and extensionality rules. The user needs only provide the equality rules they wish to use, after which the algorithm devises an appropriate notion of normal form. We will also take a peek at how the implementation of the equality checking algorithm is used in the Andromeda 2 prover.
This is joint work with Andrej Bauer and Philipp Haselwarter.