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.

Research group

Updated September 2022.

• Jana Dunfield (Assistant Professor)
• Dimitrios Economou (PhD student)
• December Stuart (MSc student)

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

Unpublished work

• Dimitrios J. Economou, Neel Krishnaswami, and Jana Dunfield. Focusing on liquid refinement typing. Draft paper, arXiv:2209.13000 [cs.PL], September 2022.

Recent papers

• Jana Dunfield and Neel Krishnaswami. Bidirectional typing. ACM Computing Surveys 54(5), May 2021.
  
  Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner’s local type inference to the present day, and provide guidance for future investigations.
• Jana Dunfield and Neel Krishnaswami. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. POPL 2019; arXiv:1601.05106.