Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14, author = {Zeuner, Max and M\"{o}rtberg, Anders}, title = {{A Univalent Formalization of Constructive Affine Schemes}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {14:1--14:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14}, URN = {urn:nbn:de:0030-drops-184574}, doi = {10.4230/LIPIcs.TYPES.2022.14}, annote = {Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Taichi Uemura. Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{uemura:LIPIcs.FSCD.2023.5, author = {Uemura, Taichi}, title = {{Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.5}, URN = {urn:nbn:de:0030-drops-179897}, doi = {10.4230/LIPIcs.FSCD.2023.5}, annote = {Keywords: Homotopy type theory, ∞-logos, ∞-topos, oplax limit, Artin gluing, modality, synthetic Tait computability, logical relation} }
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 7:1-7:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{booij_et_al:LIPIcs.TYPES.2016.7, author = {Booij, Auke B. and Escard\'{o}, Mart{\'\i}n H. and Lumsdaine, Peter LeFanu and Shulman, Michael}, title = {{Parametricity, Automorphisms of the Universe, and Excluded Middle}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {7:1--7:14}, 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.7}, URN = {urn:nbn:de:0030-drops-98554}, doi = {10.4230/LIPIcs.TYPES.2016.7}, annote = {Keywords: relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mat} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 5:1-5:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2017.5, author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu}, title = {{Displayed Categories}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.5}, URN = {urn:nbn:de:0030-drops-77220}, doi = {10.4230/LIPIcs.FSCD.2017.5}, annote = {Keywords: Category theory, Dependent type theory, Computer proof assistants, Coq, Univalent mathematics} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 8:1-8:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{ahrens_et_al:LIPIcs.CSL.2017.8, author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir}, title = {{Categorical Structures for Type Theory in Univalent Foundations}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.8}, URN = {urn:nbn:de:0030-drops-76960}, doi = {10.4230/LIPIcs.CSL.2017.8}, annote = {Keywords: Categorical Semantics, Type Theory, Univalence Axiom} }
Feedback for Dagstuhl Publishing