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-dev.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 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic Integral Cohomology in Cubical Agda. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{brunerie_et_al:LIPIcs.CSL.2022.11, author = {Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders}, title = {{Synthetic Integral Cohomology in Cubical Agda}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.11}, URN = {urn:nbn:de:0030-drops-157310}, doi = {10.4230/LIPIcs.CSL.2022.11}, annote = {Keywords: Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{danielsson:LIPIcs.TYPES.2019.10, author = {Danielsson, Nils Anders}, title = {{Higher Inductive Type Eliminators Without Paths}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {10:1--10:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-158-0}, ISSN = {1868-8969}, year = {2020}, volume = {175}, editor = {Bezem, Marc and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.10}, URN = {urn:nbn:de:0030-drops-130749}, doi = {10.4230/LIPIcs.TYPES.2019.10}, annote = {Keywords: Cubical Agda, higher inductive types} }
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-dev.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 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5, author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders}, title = {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {5:1--5:34}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5}, URN = {urn:nbn:de:0030-drops-84754}, doi = {10.4230/LIPIcs.TYPES.2015.5}, annote = {Keywords: univalence axiom, dependent type theory, cubical sets} }
Feedback for Dagstuhl Publishing