Talks

• Computational Proofs in Synthetic Homotopy Theory - invited talk at Homotopy Type Theory and Computing - Classical and Quantum 2024.
• Computational Synthetic Homotopy Theory - invited talk at Second International Conference on Homotopy Type Theory 2023.
• Computational Proofs in Cubical Type Theories - invited talk at EuroProofNet WG6 meeting 2023.
• Formalizing π₄(S³) and computing a Brunerie number in Cubical Agda - at Workshop in Honour of Thierry Coquand’s 60th Birthday 2022.
• Cubical Methods in Homotopy Type Theory and Univalent Foundations - Topos Institute Colloquium 2021.
• A Structure Identity Principle in Cubical Agda - given at the Memorial Conference for Erik Palmgren 2020.
• Programming and Proving with the Structure Identity Principle in Cubical Agda - given in Pittsburgh’s HoTT seminar 2020.
• Cubical Agda - given in the Every Proof Asssistant online seminar 2020.
• Unifying Cubical Set Models of Homotopy Type Theory - given in the HoTTest online seminar 2019.
• A Unifying Cartesian Cubical Set Model - given at MLoC 2019. Extended version of the HoTT 2019 talk.
• A Unifying Cartesian Cubical Set Model - given at HoTT 2019.
• Cubical Methods in HoTT/UF - course given at the 2019 HoTT Summer School at Carnegie Mellon University. Lecture notes still under preparation.
• Fundamentals of Coq - lecture given at the 2019 School and Workshop on Univalent Mathematics at the University of Birgmingham.
• 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.