π» π³ π· πΌ Welcome to my PL garden πΉ π± πΊ πΏ 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 PL oriented proof assistant π± I am also working on a page about implementing various small type systems and languages. Hopefully to be seen soon.