Equality Checking for General Type Theories in Andromeda 2

DOI10.1007/978-3-030-52200-1_25zbMath1503.68287OpenAlexW3041607292MaRDI QIDQ5041060

Andrej Bauer, Philipp G. Haselwarter, Anja Petković

Publication date: 13 October 2022

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-52200-1_25

zbMATH Keywords

proof assistantdependent type theoryalgorithmic equality checking

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Related Items (1)

An extensible equality checking algorithm for dependent type theories

Uses Software

• Lean
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• On Irrelevance and Algorithmic Equality in Predicative Type Theory
• The Lean Theorem Prover (System Description)
• A Modular Type Reconstruction Algorithm
• Extensional equivalence and singleton types

This page was built for publication: Equality Checking for General Type Theories in Andromeda 2