Equality Checking for General Type Theories in Andromeda 2

Autor:	Andrej Bauer, Anja Petkovic, Philipp G. Haselwarter
Rok vydání:	2020
Předmět:	Andromeda Type theory Generalization Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computation Extensionality Proof assistant Calculus Gas meter prover Type (model theory)
Zdroj:	Lecture Notes in Computer Science ISBN: 9783030521998 ICMS
DOI:	10.1007/978-3-030-52200-1_25
Popis:	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-Lof type theory, and we implemented it in the Andromeda 2 prover.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::d0bd368f648536869e1e8ae189c36a69 https://doi.org/10.1007/978-3-030-52200-1_25 Zobrazit plný text záznamu