Equality Checking for General Type Theories in Andromeda 2

We designed a user-extensible judgemental equality checking algorithm for general 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. The algor...

Descripción completa

Detalles Bibliográficos
Autores principales: Bauer, Andrej, Haselwarter, Philipp G., Petković, Anja
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7340924/
http://dx.doi.org/10.1007/978-3-030-52200-1_25
Descripción
Sumario:We designed a user-extensible judgemental equality checking algorithm for general 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. The algorithm is a generalization of type-directed equality checking for Martin-Löf type theory, and we implemented it in the Andromeda 2 prover.

Ejemplares similares