# My talks

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).

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.