I build small programming languages, theorem provers, and other systems related to PLT concepts.
I sometimes write about the things I learn βοΈ in my digital notepad π
The latest published post was a report on Propositions as Types β
I am currently working on a toy proof assistant for a little bit more than FOL π±
I am also working on a page about implementing various small type systems and languages. Hopefully to be seen soon.