Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 47:1-47:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{sterling_et_al:LIPIcs.CSL.2024.47, author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars}, title = {{Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {47:1--47:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47}, URN = {urn:nbn:de:0030-drops-196901}, doi = {10.4230/LIPIcs.CSL.2024.47}, annote = {Keywords: univalent foundations, homotopy type theory, impredicative encodings, synthetic guarded domain theory, guarded recursion, higher-order store, reference 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.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 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} }
Feedback for Dagstuhl Publishing