module Authors where
About the authors🔗
This is a page where everyone who adds to the 1lab can write a little bit about themselves. I mean it: everyone can write a bit about themselves! Try to follow the format of existing profiles in the source file, and keep the description short. Don’t forget to mention your pronouns.
Amélia they/them
@plt_amy
Hi! I’m Amélia, a non-binary programmer/mathematician. I’m 21, but I’ve been programming since age 7, and doing dependently-typed programming since 14. Last year, I implemented my own cubical type theory, to figure out what it was all about.
Since then, I’ve realised that my energy would be better spent making existing type theories more accessible, and this project was the result. The 1lab grew out of a personal project formalising category theory to better my understanding of category theory, and it’s currently undergoing a rewrite from base Agda-with-K to Cubical Agda.
My other notable projects include my personal blog, where I write about type theory and the implementation of programming languages, and Amulet, a ML-family language with an advanced type system.
Hey! I’m Reed! I develop proof assistants for a living, and write a lot of Agda. I’m interested in how we can make our tools more human friendly. In that vein, I like writing various forms of automation, especially those with a more semantic flavor.
I’m Naïm. I like the computational trilogy and arguing with Agda. I hate broken links and writing about myself.