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.
- Writing Agda blog posts in literate markdown - March 19, 2019
- Elaborating Dependent (Co)pattern Matching - September 22, 2018
- The Agda's New Sorts - May 3, 2018