Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen Theorem in Lean. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{basold_et_al:LIPIcs.ITP.2024.8, author = {Basold, Henning and Bruin, Peter and Lawson, Dominique}, title = {{The Directed Van Kampen Theorem in Lean}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8}, URN = {urn:nbn:de:0030-drops-207368}, doi = {10.4230/LIPIcs.ITP.2024.8}, annote = {Keywords: Lean, Directed Topology, Van Kampen Theorem, Directed Homotopy Theory, Formalised Mathematics} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Jelle Wemmenhove, Cosmin Manea, and Jim Portegies. Classification of Covering Spaces and Canonical Change of Basepoint. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{wemmenhove_et_al:LIPIcs.TYPES.2023.1, author = {Wemmenhove, Jelle and Manea, Cosmin and Portegies, Jim}, title = {{Classification of Covering Spaces and Canonical Change of Basepoint}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {1:1--1:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.1}, URN = {urn:nbn:de:0030-drops-204795}, doi = {10.4230/LIPIcs.TYPES.2023.1}, annote = {Keywords: Synthetic Homotopy Theory, Homotopy Type Theory, Covering Spaces, Change-of-Basepoint Isomorphism} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Maximilian Doré, Evan Cavallo, and Anders Mörtberg. Automating Boundary Filling in Cubical Agda. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dore_et_al:LIPIcs.FSCD.2024.22, author = {Dor\'{e}, Maximilian and Cavallo, Evan and M\"{o}rtberg, Anders}, title = {{Automating Boundary Filling in Cubical Agda}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.22}, URN = {urn:nbn:de:0030-drops-203514}, doi = {10.4230/LIPIcs.FSCD.2024.22}, annote = {Keywords: Cubical Agda, Automated Reasoning, Constraint Satisfaction Programming} }
Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.13, author = {Cavallo, Evan and Harper, Robert}, title = {{Internal Parametricity for Cubical Type Theory}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {13:1--13:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.13}, URN = {urn:nbn:de:0030-drops-116564}, doi = {10.4230/LIPIcs.CSL.2020.13}, annote = {Keywords: parametricity, cubical type theory, higher inductive types} }
Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.14, author = {Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W}, title = {{Unifying Cubical Models of Univalent Type Theory}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.14}, URN = {urn:nbn:de:0030-drops-116578}, doi = {10.4230/LIPIcs.CSL.2020.14}, annote = {Keywords: Cubical Set Models, Cubical Type Theory, Homotopy Type Theory, Univalent Foundations} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 31:1-31:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{sterling_et_al:LIPIcs.FSCD.2019.31, author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel}, title = {{Cubical Syntax for Reflection-Free Extensional Equality}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {31:1--31:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31}, URN = {urn:nbn:de:0030-drops-105387}, doi = {10.4230/LIPIcs.FSCD.2019.31}, annote = {Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Kuen-Bang Hou (Favonia) and Robert Harper. Covering Spaces in Homotopy Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{hou(favonia)_et_al:LIPIcs.TYPES.2016.11, author = {Hou (Favonia), Kuen-Bang and Harper, Robert}, title = {{Covering Spaces in Homotopy Type Theory}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {11:1--11:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.11}, URN = {urn:nbn:de:0030-drops-98512}, doi = {10.4230/LIPIcs.TYPES.2016.11}, annote = {Keywords: homotopy type theory, covering space, fundamental group, mechanized reasoning} }
Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{angiuli_et_al:LIPIcs.CSL.2018.6, author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert}, title = {{Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {6:1--6:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6}, URN = {urn:nbn:de:0030-drops-96734}, doi = {10.4230/LIPIcs.CSL.2018.6}, annote = {Keywords: Homotopy Type Theory, Two-Level Type Theory, Computational Type Theory, Cubical Sets} }
Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{hou(favonia)_et_al:LIPIcs.CSL.2016.22, author = {Hou (Favonia), Kuen-Bang and Shulman, Michael}, title = {{The Seifert-van Kampen Theorem in Homotopy Type Theory}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {22:1--22:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.22}, URN = {urn:nbn:de:0030-drops-65626}, doi = {10.4230/LIPIcs.CSL.2016.22}, annote = {Keywords: homotopy type theory, fundamental group, homotopy pushout, mechanized reasoning} }
Feedback for Dagstuhl Publishing