Talks
- From signatures to monads in UniMath - invited talk at SSTT 2017.
- Cubical Type Theory: a constructive interpretation of the univalence axiom - invited talk at TTT 2017.
- Cubical Type Theory - talk at the ICMS 2016 session on Univalent Foundations and Proof Assistants.
- Cubical Type Theory: a constructive interpretation of the univalence axiom - invited talk at HoTT/UF 2016.
- Cubical Type Theory: a constructive interpretation of the univalence axiom - given at the Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics at the Fields institute 2016. This talk focuses on Glue types and the proof of the univalence axiom in cubicaltt.
- Cubical Type Theory: a constructive interpretation of the univalence axiom - given at the PLDG seminar at Cornell 2016.
- Computer algebra systems, formal proofs and interactive theorem proving - Mathematical Conversation at the IAS 2016.
- Type Theory and Formalization of Mathematics - given to a general audience of mathematicians at the IAS 2015.
- An Implementation of a Cubical Type Theory - given at AIM XXI 2015.
- A Coq Formalization of Finitely Presented Modules - given at ITP 2014.
- Formalizing Elementary Divisor Rings in Coq - given at MAP 2014.
- Formalization of Mathematics - given at the ProgLog workshop 2014.
- Coherent and Strongly Discrete Rings in Type Theory - given at CPP 2012.
- A Formal Proof of Sasaki-Murao Algorithm - given at MAP 2012.
- Rings with Explicit Divisibility Formalized in Coq - given at TYPES 2011.
- Formalization of Rings with Explicit Divisibility in Type Theory - given at the ProgLog workshop 2011.
- Homology of Simplicial Complexes in Haskell - given at the Programming Logic Seminar at Chalmers 2010.
- An overview of the SSReflect extension to the Coq system - given at the Programming Logic Seminar at Chalmers 2010.
- Constructive Algebra in Functional Programming and Type Theory - given at MAP 2010.