Paid Undergrad Internship in Canada - Dependent Types

Stream: job postings

[Joey Eremondi]

If you know undergraduates who are interested in dependent types (or are one), I'm looking for students to do a 12-week paid internship in Canada during the Summer of 2026, as part of the MITACS GlobalLink program.

The program is specifically looking for students from outside of Canada, who will have 1-3 semesters left in their program as of Fall 2026, who are from one of the following countries: Brazil, Chile, China, Colombia, France, Germany, Hong Kong, Jordan, Mexico, Pakistan, Singapore, South Korea, Taiwan, Thailand, Tunisia, Ukraine, United Kingdom and the United States

The projects I'm looking for students are:

• Flexible Pattern Matching in Dependently Typed Languages
• A Corpus of Error Messages from Dependently Typed Compilers
• Implementing Gradual Dependent Types in Idris or Lean

Students can apply to multiple projects at multiple universities and rank them by preference.

Interested students can apply here: https://globalink.mitacs.ca/#/student/application/welcome

The full eligibility requirements are here: https://www.mitacs.ca/our-programs/globalink-research-internship-students/

And any questions about the projects can be directed to me at jeremondi@uregina.ca.
--

Dr. Joseph Eremondi
Assistant Professor, Department of Computer Science,
University of Regina, Saskatchewan, Canada
https://eremondi.com
he/him

[Alok Singh]

Gradual dependent types in Lean would be awesome