module Authors where


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 19, 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.