Chase Norman. Canonical (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24703,
title = {{Canonical}},
author = {Norman, Chase},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:06a599989bad108dc52bfdff704d356badfa63d4;origin=https://github.com/chasenorman/Canonical;visit=swh:1:snp:b14b45164fd97819d6c472ac9195bf01ab92047c;anchor=swh:1:rev:d5c7fd0d8d0f1a2e4d8eed817d534725ea8e1156}{\texttt{swh:1:dir:06a599989bad108dc52bfdff704d356badfa63d4}} (visited on 2025-09-22)},
url = {https://github.com/chasenorman/Canonical},
doi = {10.4230/artifacts.24703},
}
Chase Norman. CanonicalLean (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24708,
title = {{CanonicalLean}},
author = {Norman, Chase},
note = {Software, version v4.22.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:98f9920f9b96cabe1c6188b23fd3823d0ad9fb0f;origin=https://github.com/chasenorman/Canonicallean;visit=swh:1:snp:944ef1c9397eb4eb6dc2e6e7d500f38c3033a5ea;anchor=swh:1:rev:65797c0994b252ecca26934afe92766147fedbd3}{\texttt{swh:1:dir:98f9920f9b96cabe1c6188b23fd3823d0ad9fb0f}} (visited on 2025-09-22)},
url = {https://github.com/chasenorman/CanonicalLean},
doi = {10.4230/artifacts.24708},
}
Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)
Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
author = {Norman, Chase and Avigad, Jeremy},
title = {{Canonical for Automated Theorem Proving in Lean}},
booktitle = {16th International Conference on Interactive Theorem Proving (ITP 2025)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-396-6},
ISSN = {1868-8969},
year = {2025},
volume = {352},
editor = {Forster, Yannick and Keller, Chantal},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14},
URN = {urn:nbn:de:0030-drops-246128},
doi = {10.4230/LIPIcs.ITP.2025.14},
annote = {Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Feedback for Dagstuhl Publishing