I am recruiting applicants for a funded PhD student position in the Theory of Programming Languages at the University of Regina in Regina, Canada. Broadly, I’m looking for anyone who is interested in making dependently typed languages and proof assistants easier to use.

Specific areas of interest include (but are not limited to):

• Programming with dependently typed languages, like Lean, Agda, Idris, and Coq
• Improving usability of dependently typed programming languages
• Gradual types and gradual dependent types
• Live programming environments for dependent types
• Static analysis of dependently typed programs
• Ordinal notations and termination proofs
• Error messages and repair suggestions for static and dynamic type errors
• Dependent pattern matching - semantics and implementation

Graduate students at the U of R have the opportunity to be part of a small, focused research group where you can work closely with your advisor. Regina is one of Canada’s most affordable cities to live in, and students have access to Canada’s universal health care. The stipend is roughly $23000-$28000 CAD per year, from a mix of research and teaching-assistantships. Students will have the opportunity to gain experience as a Teaching Assistant or Sessional Lecturer.

The deadline for applications is June 15, though out-of-cycle applications are possible. The target start date is January of 2026. Earlier start dates are possible, but may be difficult for non-residents of Canada due to visa processing times.

For more information on applying, visit https://www.uregina.ca/science/cs/graduate/future-grad/index.html. Any questions for me specifically can be directed to me by email.