PL 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.