The 36th Implementors' Meeting will happen in Delft on 10-16 May! Find all the details and register at Proposals for talks, discussions, and code sprints are welcome too!

2.6.3 has (finally) been released! Get yours now at and get a complimentary performance boost to your Agda code FOR FREE!

Listening to the Type Theory Forall podcast with Kevin Buzzard (@xenaproject). Really interesting view on how theorem provers are viewed in mathematics and where formal mathematics is heading. It's making me think about what the Agda community could learn from this. Strongly recommended you give it a listen!

I didn't expect we would ever see a replacement of 's oldest components, but here it is:

New PR for adding explicit polarity annotations to : Really looking forward to having this, check it out!

Just one of the very exciting code sprints at the meeting in Edinburgh: explicit polarity annotations (screenshot posted by Josselin Poiret on Zulip).

I'm a programming languages researcher who works on bringing ideas from dependent type theory into practice. I am also one of the core developers of the dependently typed programming language slash proof assistant. I am currently assistant professor in the Programming Languages group at TU Delft.

I blog very irregularly about Agda and stuff on my website:

In my free time, I play clarinet and bassoon and role-playing games of the tabletop variety. I'm also a proud member of Giving What We Can.

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.