Theory and Practice of Programming Languages (TPPL)

Programming languages (PL) are the basis of computing. We study what programs mean, in a very broad sense.

One kind of meaning is about what programs do specifically: what happens when you run a given program on a given input? What output does it produce, what files does it modify, what does it send over the network, how long does it take to run?

Another kind of meaning is about what programs are, or about what programs do in general. For example, if you write a Java method that takes two integers x and y as parameters, and the Java compiler accepts the program, the values must be integers. If another method tried to pass a String, you would get a type error.

Testing can show the presence of bugs but not their absence; types can show the absence of bugs (usually not all bugs, but a large number of them). Types reach beyond what a program does on a single input or set of inputs. That is what makes type systems useful.

However, computer science is not just about being useful, and neither are type systems. Rather, type systems have deep connections to the formal theories of mathematical logic, particularly natural deduction, the λ-calculus, and combinatory logic. Just as modular software design is about elegantly combining smaller pieces to create a whole, natural deduction elegantly combines smaller pieces of reasoning. All of this work in logic began before modern computer science, but turned out to be extraordinarily useful for type systems, compilers, and formal verification.

Our research investigates questions such as the following:

Investigating these questions requires us to apply a variety of research techniques:

Research group

Updated December 2020.

We are recruiting students at all levels (undergrad, MSc, PhD) for 2021. If you are interested in the kind of research we do, please get in touch (jana at cs queensu ca). To ensure that your message is read, please include the following in the subject line: TPPL.

Recent papers