Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2024.10, author = {Kaposi, Ambrus and Xie, Szumi}, title = {{Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {10:1--10:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.10}, URN = {urn:nbn:de:0030-drops-203396}, doi = {10.4230/LIPIcs.FSCD.2024.10}, annote = {Keywords: Type theory, universal algebra, inductive types, quotient inductive types, higher-order abstract syntax, logical framework} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{matthes_et_al:LIPIcs.FSCD.2024.25, author = {Matthes, Ralph and Wullaert, Kobe and Ahrens, Benedikt}, title = {{Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {25:1--25:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.25}, URN = {urn:nbn:de:0030-drops-203540}, doi = {10.4230/LIPIcs.FSCD.2024.25}, annote = {Keywords: Non-wellfounded syntax, Substitution, Monoidal categories, Actegories, Tensorial strength, Proof assistant Coq, UniMath library} }
Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Gun Pinyo and Nicolai Kraus. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{pinyo_et_al:LIPIcs.TYPES.2019.5, author = {Pinyo, Gun and Kraus, Nicolai}, title = {{From Cubes to Twisted Cubes via Graph Morphisms in Type Theory}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {5:1--5: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.5}, URN = {urn:nbn:de:0030-drops-130694}, doi = {10.4230/LIPIcs.TYPES.2019.5}, annote = {Keywords: homotopy type theory, cubical sets, directed equality, graph morphisms} }
Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{altenkirch_et_al:LIPIcs.CSL.2016.21, author = {Altenkirch, Thorsten and Capriotti, Paolo and Kraus, Nicolai}, title = {{Extending Homotopy Type Theory with Strict Equality}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {21:1--21:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.21}, URN = {urn:nbn:de:0030-drops-65612}, doi = {10.4230/LIPIcs.CSL.2016.21}, annote = {Keywords: homotopy type theory, coherences, strict equality, homotopy type system} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 359-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{capriotti_et_al:LIPIcs.CSL.2015.359, author = {Capriotti, Paolo and Kraus, Nicolai and Vezzosi, Andrea}, title = {{Functions out of Higher Truncations}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {359--373}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.359}, URN = {urn:nbn:de:0030-drops-54257}, doi = {10.4230/LIPIcs.CSL.2015.359}, annote = {Keywords: homotopy type theory, truncation elimination, constancy on loop spaces} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{ahrens_et_al:LIPIcs.TLCA.2015.17, author = {Ahrens, Benedikt and Capriotti, Paolo and Spadotti, R\'{e}gis}, title = {{Non-Wellfounded Trees in Homotopy Type Theory}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {17--30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.17}, URN = {urn:nbn:de:0030-drops-51522}, doi = {10.4230/LIPIcs.TLCA.2015.17}, annote = {Keywords: Homotopy Type Theory, coinductive types, computer theorem proving, Agda} }