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 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} }