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-dev.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-dev.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-dev.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} }
Feedback for Dagstuhl Publishing