I’m a mathematician with an interest in programming language theory and type theory in particular. I'm currently doing a postdoc in the Programming Logic group in Göteborg, where I work on Agda, a programming language and proof assistant based on Martin-Löf type theory.
- Hack your type theory with rewrite rules - October 21, 2019
- Formalize all the things (in Agda) - October 4, 2019
- EUTYPES '19 Summer School in Ohrid - September 13, 2019
- Writing Agda blog posts in literate markdown - July 9, 2019
- Elaborating Dependent (Co)pattern Matching - September 22, 2018
- The Agda's New Sorts - May 3, 2018