Turing-Completeness of Polymorphic Stream Equation Systems (RTA 2013, with Florent Balestrieri)
First year report, contains unpublished results mentioned under Further Work in the above article.
Turing-Completeness of Polymorphic Stream Equation Systems (talk, based on joint work with Florent Balestrieri)
Quotient Container Antiderivatives of Cyclic Actions
Isomorphism of Finitary Inductive Types (talk)
Equations Over Groups (talk)
On the Hierarchy of Univalent Universes: U(n) is not n-Truncated (submitted to TOCL, with Nicolai Kraus)
Formalization of the results of the above article in Agda.
How To Create a Doubly-Linked Dodecahedron
On the Merits of the Eta-Law for Inductive Types
School of Computer Science and Information Technology Home Page
The University of Nottingham Home Page