Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
András Kovács. Generalized Universe Hierarchies and First-Class Universe Levels. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 28:1-28:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{kovacs:LIPIcs.CSL.2022.28, author = {Kov\'{a}cs, Andr\'{a}s}, title = {{Generalized Universe Hierarchies and First-Class Universe Levels}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {28:1--28:17}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.28}, URN = {urn:nbn:de:0030-drops-157485}, doi = {10.4230/LIPIcs.CSL.2022.28}, annote = {Keywords: type theory, universes} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{kaposi_et_al:LIPIcs.TYPES.2019.6, author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s and Lafont, Ambroise}, title = {{For Finitary Induction-Induction, Induction Is Enough}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {6:1--6:30}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.6}, URN = {urn:nbn:de:0030-drops-130707}, doi = {10.4230/LIPIcs.TYPES.2019.6}, annote = {Keywords: type theory, inductive types, inductive-inductive types} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25, author = {Kaposi, Ambrus and Huber, Simon and Sattler, Christian}, title = {{Gluing for Type Theory}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {25:1--25:19}, 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.25}, URN = {urn:nbn:de:0030-drops-105323}, doi = {10.4230/LIPIcs.FSCD.2019.25}, annote = {Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types} }
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 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Ambrus Kaposi and András Kovács. A Syntax for Higher Inductive-Inductive Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 20:1-20:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2018.20, author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s}, title = {{A Syntax for Higher Inductive-Inductive Types}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.20}, URN = {urn:nbn:de:0030-drops-91906}, doi = {10.4230/LIPIcs.FSCD.2018.20}, annote = {Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations} }
Feedback for Dagstuhl Publishing