mastodon 4.8.0-alpha.2+glitchPL postdoc. Currently a Newton International Fellow at the University of Edinburgh. Soon to be Assistant Prof. at University of Regina, starting July 2024. Formerly PhD at UBC with Ron Garcia
Broadly interested in making it easier to prove software correct with dependent types. Projects include dependent pattern matching, gradual dependent types, and error message generation.
I gave a talk at Strathclyde on gradual dependent types. It covered a lot of the same material as my thesis defence, but a lot more in depth. I assumed the audience knew/appreciated dependent types, and I had a whole hour to talk.
Thanks to @gallais@mamot.fr for inviting me!