Author of the publication

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.

, , and . CSL, volume 119 of LIPIcs, page 6:1-6:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2018)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Covering Spaces in Homotopy Type Theory., and . TYPES, volume 97 of LIPIcs, page 11:1-11:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2016)The Seifert-van Kampen Theorem in Homotopy Type Theory., and . CSL, volume 62 of LIPIcs, page 22:1-22:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2016)Computational Higher Type Theory III: Univalent Universes and Exact Equality., , and . CoRR, (2017)A Note on the Uniform Kan Condition in Nominal Cubical Sets., and . CoRR, (2015)Correctness of compiling polymorphism to dynamic typing., , and . J. Funct. Program., (2017)Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities., , and . CSL, volume 119 of LIPIcs, page 6:1-6:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2018)A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory., , , and . LICS, page 565-574. ACM, (2016)Syntax and models of Cartesian cubical type theory., , , , , and . Math. Struct. Comput. Sci., 31 (4): 424-468 (2021)An Order-Theoretic Analysis of Universe Polymorphism., , and . Proc. ACM Program. Lang., 7 (POPL): 1659-1685 (January 2023)Logarithm and program testing., and . Proc. ACM Program. Lang., 6 (POPL): 1-26 (2022)