# Talks

- Higher Inductive Types in Cubical Type Theories - given at EUTypes 2018.
- On Higher Inductive Types in Cubical Type Theory - given at LICS 2018.
- Yet Another Cartesian Cubical Type Theory - talk given at Types, Homotopy Type theory, and Verification at the Hausdorff institute in Bonn, 2018.
- Cubical variations: HITs, pi4(s3) and yacctt - talk at MURI meeting 2018 on HITs in cubicaltt, attempts to compute the Brunerie number and recent work on a “formal” version of Computational Higher Type Theory called yacctt (Yet Another Cubical Type Theory).
- A hands-on introduction to cubicaltt - series of lectures on cubicaltt given at Inria Sophia Antipolis (May-June 2017) and in the HoTT seminar at Carnegie Mellon University (Nov-Dec 2017). I summarized these in a blog post on the Homotopy Type Theory blog.
- 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.