Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper 0001
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities
CSL, 2018.
@inproceedings{CSL-2018-AngiuliF0, author = "Carlo Angiuli and Kuen-Bang Hou (Favonia) and Robert Harper 0001", booktitle = "{Proceedings of the 27th EACSL Annual Conference on Computer Science Logic}", doi = "10.4230/LIPIcs.CSL.2018.6", isbn = "978-3-95977-088-0", pages = "17", publisher = "{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}", title = "{Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities}", year = 2018, }