My talks

June 2024. Programming and Proving in Agda. Advanced Track at ZuriHac 2024 (video).

April 2024. Agda Core: The Dream and the Reality. Talk at the IFIP WG2.8 meeting (slides).

November 2022. Connecting Agda to other theorem provers via EuroProofNet. Talk at the 31nd Agda Meeting in Edinburgh (slides).

June 2022. How to write a translator to Dedukti: The case of Agda. Lecture at the 1st Dedukti school in Nantes (colocated with TYPES 2022) (slides).

July 2021. The quest for modular confluence of rewrite rules in type theory. Invited talk at the 10st International Workshop on Confluence (online) (slides) (video).

October 2020. Rewriting Type Theory. Invited talk at the Scottish Programming Language Seminar (slides) (video).

October 2020. Agda Core: Where do we come from and where do we go?. Talk at the 33rd Agda Meeting (online) (slides).

July 2020. Rewriting Type Theory. Talk at the UF session of ICMS 2020 (slides).

December 2019. Type Theory Unchained. Talk at PLNL 2019 (slides).

March 2019. How to tame your rewrite rules. Talk at the 29nd Agda Meeting in Tokyo (slides).

March 2019. Verifying five Haskell libraries with Agda2Hs. Talk at the 24nd Agda Meeting (online) (slides).

February 2019. Edit-time tactics for Agda. Talk at Petit-déj Galinette in Nantes (slides).

March 2018. Elaborating dependent (co)pattern matching. Talk at the 2nd Göteborg-Stockholm Type Theory Seminar in Stockholm (slides).

September 2017. Depending on equations: A proof-relevant framework for unification in dependent type theory. Invited talk at the 31st International Workshop on Unification in Oxford (slides).

April 2016. A sound unification algorithm based on telescope equivalences. Talk at the 23rd Agda Meeting in Glasgow (slides).

September 2015. STAMP: Strongly Type-sAfe Meta-Programming. Talk at the 22nd Agda Meeting in Leuven (slides).

June 2015. Unification in a context of postponed equations. Talk at the 21st Agda Meeting in Göteborg (slides).

May 2014. Eliminating dependent pattern matching without K. Talk at the 19nd Agda Meeting in Paris.