An extensible equality checking algorithm for dependent type theories

zbMath1504.68276arXiv2103.07397MaRDI QIDQ5028472

Anja Petković Komel, Andrej Bauer

Publication date: 9 February 2022

Full work available at URL: https://arxiv.org/abs/2103.07397

zbMATH Keywords

type theoryproof assistantequality checking

Mathematics Subject Classification ID

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

Related Items (1)

Finitary type theories with and without contexts

Uses Software

• Lean

Cites Work

• Unnamed Item
• The locally nameless representation
• On Irrelevance and Algorithmic Equality in Predicative Type Theory
• Interacting with Modal Logics in the Coq Proof Assistant
• The Lean Theorem Prover (System Description)
• A Modular Type Reconstruction Algorithm
• Equality Checking for General Type Theories in Andromeda 2
• Extensional equivalence and singleton types

This page was built for publication: An extensible equality checking algorithm for dependent type theories