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
_version_ 1783555123464634368
author Bauer, Andrej
Haselwarter, Philipp G.
Petković, Anja
author_facet Bauer, Andrej
Haselwarter, Philipp G.
Petković, Anja
author_sort Bauer, Andrej
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7340924
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73409242020-07-08 Equality Checking for General Type Theories in Andromeda 2 Bauer, Andrej Haselwarter, Philipp G. Petković, Anja Mathematical Software – ICMS 2020 Article 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. 2020-06-06 /pmc/articles/PMC7340924/ http://dx.doi.org/10.1007/978-3-030-52200-1_25 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Bauer, Andrej
Haselwarter, Philipp G.
Petković, Anja
Equality Checking for General Type Theories in Andromeda 2
title Equality Checking for General Type Theories in Andromeda 2
title_full Equality Checking for General Type Theories in Andromeda 2
title_fullStr Equality Checking for General Type Theories in Andromeda 2
title_full_unstemmed Equality Checking for General Type Theories in Andromeda 2
title_short Equality Checking for General Type Theories in Andromeda 2
title_sort equality checking for general type theories in andromeda 2
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7340924/
http://dx.doi.org/10.1007/978-3-030-52200-1_25
work_keys_str_mv AT bauerandrej equalitycheckingforgeneraltypetheoriesinandromeda2
AT haselwarterphilippg equalitycheckingforgeneraltypetheoriesinandromeda2
AT petkovicanja equalitycheckingforgeneraltypetheoriesinandromeda2

Ejemplares similares