Theory and Practice of Programming Languages

Programming languages (PL) are the basis of computing. I 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.

My research investigates questions such as the following:

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

If you are interested in doing research at the undergraduate, master's, or PhD levels, and any of the above research questions sound interesting to you, please get in touch (joshuad at cs queensu ca). To ensure that I read your message, please include the following in the subject line: TPPL. Thank you!