Dr. Joseph Eremondi

MITACS Internships in Programming Languages

August 05, 2026

The MITACS GlobalLink program allows undergraduate students from across the world to complete paid research internships at Canadian universities. The internships last 12 weeks, with start dates between May 1 and July 31.

For 2027, there are several programming-language centred projects which are accepting applications.

Project Titles

Eligibility

  • Applicants must be from one of the following partner countries: Austria, Brazil, Chile, China, Colombia, Finland, France, Germany, Hong Kong, India, Jordan, Mexico, Pakistan, Peru, Singapore, South Korea, Taiwan, Thailand, Tunisia, Ukraine, United Kingdom, United States
  • Applicants must be full-time undergraduate students with between one and three semesters remaining in their program as of Fall 2027.
  • Full eligibility requirements can be found at the MITACS page

How to Apply

  • Applications are due September 16 at 1pm Pacific Time
  • This page has full application instructions

Project Details

Equivalence Checking of Database Queries

Equivalence checking of database queries has various applications, such as validating query optimizations, automated query grading, detecting redundant queries, and improving the reliability of database applications. While prior work has explored different approaches to equivalence checking for database queries, existing techniques often focus on relational databases and a limited set of query operators. There is still limited support for different data models, such as document databases and graph databases. This limitation reduces the applicability of current equivalence-checking tools in realistic settings where applications combine heterogeneous data models and complex query features. This research project aims to explore techniques that address these gaps and make equivalence checking more broadly applicable across modern database systems.

Programmable Pattern Matching for Proof Assistants

Pattern matching provides a convenient way to write functional programs that exhaustively handle all inputs. In dependently typed programming languages, pattern matching corresponds to the “proof by cases” technique, allowing a programmer to write a function by specifying the output for each possible shape the input might have. However, pattern matching in dependently typed languages is often quite limited: the cases must directly correspond to the constructors of a datatype, and support for overlapping or catch-all cases tends to be poor.

Recent work has developed a theory of pattern matching based on coverage semantics, where the exact set of patterns which is allowed is treated as a parameter of the language. Sheaf theory is used to provide the criteria for which patterns lead to a well-defined semantics for matching. Coverage semantics capture the status quo for pattern matching, but also enable more exotic forms of matching, such as matching on arbitrary isomorphisms.

This project aims to develop a prototype of “pattern matching as a library,” based on an internal variant of coverage semantics. In a proof assistant such as Agda, Idris, or Lean, we will develop a library for pattern matching which is parameterized over the set of allowed patterns. This will provide a testbed for novel pattern-matching variants, without requiring major changes to the implementation of a proof assistant. To use the library, the programmer initially provides a predicate defining allowed pattern-sets, along with a proof that this meets the sheaf-theoretic criterion for leading to well defined semantics. The function for pattern matching will take a list of patterns, a result for each pattern, and a proof that the set of patterns satisfy the earlier provided predicate.

GPU/Multicore Unification for Functional Languages

Unification is a useful tool for looking at two structures containing variables, and to determine what values the variables must have for the structures to be the same. Higher-order unification extends this to functions/programs, finding what substitution will make two programs behave identically on all inputs. Higher order unification is a key part of dependent type checking and proof inference, and is a key part of the implementation of proof assistants like Lean, Rocq and Agda. While higher-order unification is undecidable in general, large fragments of it can be computed in finite time.

The goal of the project is to write an implementation of higher-order unification which can be easily parallelized, either to use multiple cores of a CPU, to be distributed across multiple computers, or to use specialized features of a GPU. Unification is often one of the most expensive parts of typechecking in proof assistants, so the ability to parallelize it could lead to performance improvements for type checking and proof search.

Depending on the student’s background, a parallel implementation could use a specialized functional language for parallel computing like Futhark or MPL, or a parallel-computing library for a general purpose language, such as Haskell’s Accelerate or Rust’s Rayon.

A key part of the project will be evaluating the degree to which it is even possible to parallelize unification. Most implementations of unification rely heavily on recursion and a global shared constraint list, which will be bottlenecks if parallelization is naively introduced. Similarly, if a GPU approach is taken, a novel representation of unification problems and constraints will be needed to fully utilize available GPU operations.

Optional Termination Checking for Proof Assistants

Most dependently typed languages require that all code written in such a language be obviously terminating. Usually, this means that all recursive calls must be on structurally smaller arguments, and that there can be no “type of all types.” For proof assistants and mechanized mathematics, this is critically important, since a function that runs forever can be used to write a proof of falsehood.

However, when dependent types are used to prevent bugs and guide software development, the termination checker can become more of a burden than a help. The programmer may eventually want to prove that their functions are total, but only after prototyping and testing their code. Moreover, sometimes code is terminating, but in a way that is not obvious to the compiler, so false positives can be raised. The undecidability of the halting problem means that such cases are unavoidable, but they can be difficult to debug and analyze.

This project aims to integrate a mix of static and dynamic termination checking into the Idris programming language. This would enable programmers to prototype their code without having to worry about proving termination, without completely disabling all checks. If they have accidentally introduced a potential source of non-termination, a dynamic check can raise a warning or an error, which can inform how to eventually prove termination.

There are two aspects to the project, the choice of which will depend on the background and number of students working on the project: (1) Introducing universe levels into Idris to prevent type-in-type, and having this check occur statically or dynamically. (2) Adding dynamic size-tracking to Idris, so that (a) possible infinite loops can be flagged dynamically, and (b) programmers can view dynamic traces to decide how to prove termination.

Formalizing Mathematics and Computing in Agda

Brief Description: While the library of Agda is already sizeable (https://github.com/agda/agda-stdlib for the library, and https://wiki.portal.chalmers.se/agda/pmwiki.php for more information about the system itself). I am one of the contributors to the library, and the main co-author of the Category Theory support. There is still a lot to do, both in computer science and in mathematics. Thus there is a fair amount of flexibility as to exactly what domain to work on, depending on the student’s background and preferences.

Skills: Experience programming in at least 2 programming languages, but more is better. Some functional language (such as Haskell) would be optimal. A solid background in Mathematics. Must like doing things very precisely.

Required role of the student: Implement various domains of mathematics and computer science in Agda. While the domains will be drawn from known areas, the implementations will be new, and often require novel ideas too. Some creativity (with guidance) will be needed to find good encodings of certain concepts. Looking at the current library is the best way to understand the kinds of computing and mathematics involved. But also looking at the libraries of other systems (Isabelle, Coq, Lean, Idris, etc) is also a good guide.

Long-term Software Engineering

Brief Description: Drasil is a set of tools, written in Haskell, that provides for a completely different workflow for generating correct software, as part of large certifiable program families. One of the key ingredients is code generation, which helps make the coding of traditional artifacts more portable and more reusable. Furthermore, influenced by literate programming and org-mode, we have a means of doing knowledge capture of the fundamental laws of physics, basic mathematics and methods of software construction. Once foundational knowledge has been entered, it can be infinitely re-used. This deconstruction of software into pieces finer-grained than components, classes, etc, greatly facilitates re-use by allowing many more compositions of pieces. And because the knowledge is documented, a lot of normally tedious documentation can now be generated. The result is software that is both solid and documented, without the tedium usually associated with such tasks.

The fundamental idea is to “generate all the things”. By understanding what all the artifacts that usually make up a complete piece of software – including tests, build instructions, theory manuals, user manuals, and so on – we see that they are mostly composed of the same information but arranged in different ways. Of course, this is natural and reasonable, as the pieces are indeed talking about the same software! This very repetition is the source of our compression and re-use techniques.

Skills: We are looking for solid programmers who are very eager to learn new ideas. Someone who thinks they know all there is about programming will not be happy in our project, as we deconstruct all the usual methodologies of software engineering and turn them sideways. And we use ideas from many different other disciplines; while somewhat mathematics-centric, we also use a lot of physics and dip into knowledge management, philosophy and social sciences as necessary. Eagerness to learn, as well as re-learn new ways of thinking on old ideas, is very important.

Role: The student would participate in all activities on Drasil (https://github.com/JacquesCarette/Drasil) – coding of the infrastructure (in Haskell), coding of new examples (in Drasil itself), improving old examples when new commonalities and patterns are found, as well as cooperating with all others also working on this open source project. The students have significant scope for creative contributions; we heavily encourage the students to monitor their own ‘pain points’ while working on Drasil, suggest new features for mitigating those issues, and then design and implement them. We work in a modern, github-driven environment with Travis-driven continuous integration, large test suites and generation of code in many languages (such as Java, C#, C++, Python, and Lua). New backend languages will be implemented, with the students likely participating in that effort.

One of the best ways to understand the students’ role is to look at what other students have done on the project itself – everything is completely visible on the project’s github pages. The workflow and scope of student work is entirely documented there, likely in more detail than anyone really cares to know. But this also means that we offer a ‘no surprises’ environment where what will be expected is fully visible and public.

Building Verified Quantum Programming Language Implementations

With the increase in availability and feasability of quantum computing hardware, there has been a growing importance in understanding quantum programming from the programming languages perspective. Over the past decade, a particular paradigm that has been emerging is to use a functional language to generate quantum circuits that are eventually executed on a quantum processor. One such example is the Quipper family of quantum programming languages. Unfortunately, Quipper languages have complex operational semantics: they are inherently effectful, and they rely on set-theoretic operations and fresh name generation to manipulate quantum circuits. This makes them difficult to reason about using standard programming language techniques and, ultimately, to mechanize. Recently, we introduced Proto-Quipper-A, a rational reconstruction of Proto-Quipper languages for static circuit generation. It uses a linear λ-calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. We then integarate this circuit language with a linear/non-linear functional language using a modality. The goal of this project is to build a verified language implementation of Proto-Quipper-A in Rocq and extract a stand-alone implementation and understand how to model some basic quantum algorithms with this language.

Benchmarking McPTS

Mechanizing a type theory and its meta-theory in a proof assistant establishes a high degree of trust in its correctness. However, this is also an intricate and time-consuming endeavour, since such mechanizations often exploit the specific structure of the type theory considered. This results in a patch-work of developments for a range of type theories that are similar, but still largely incompatible.

We recently built the McPTS infrastructure in the proof assistant Rocq where we uniformly describe a large family of calculi by embracing what is known as the pure type systems approach. In this view, we abstract over differences in these calculi (for example how function spaces are defined) and develop a generic consistency proof and a generic verified type checking kernel. By instantiating our development, we directly obtain normalization proofs for several important languages, including a version of \miniml, the logical framework LF, and Martin L{\“o}f type theory, as well as the corresponding verified type-checking implementations.

The goal of this project is to experimentallly compare out extracted verified type-checking implementation for logical framework LF and to the hand-crafted implementation of the LF type checker that is part of the Beluga proof assistant and the Twelf logical framework. By building benchmarks and experimentally comparing these two implementations we aim to understand how competitive the fully verified implementation is compared to existing hand-crafted implementation.

Verified Concurrent Algorithms

The MOST programming language (Kavanagh and Pientka, 2024) extends traditional session-typed languages with concurrent type-level computation to more precisely specify communication protocols. In particular, protocols specifications are very restricted concurrent programs that generate a communication protocol based on past communications in a system. MOST users write both a program and its protocol specification, and MOST’s type system ensures that the program respects its specification.

This project will use MOST to specify and verify concurrent algorithms and data structures, including stacks, queues, and concurrent hash-tries. Since concurrent algorithms and data structures are often described in terms of shared memory, they will need to be redesigned to be implemented as a collection of interacting processes. We will draw inspiration from the literature and from open-source software projects to produce other case studies. These case studies will inform future development of MOST, form a reusable library of verified concurrent algorithms, and help develop principles for specifying concurrent algorithms and data structures in this setting.