Jana Dunfield


I'm an Assistant Professor in the School of Computing at Queen’s University in Kingston, Ontario.

Before that, I was a researcher in the UBC Department of Computer Science in Vancouver, a postdoc at the Max Planck Institute for Software Systems, and a postdoc with Brigitte Pientka's Computation and Logic Group at McGill, where I worked on Beluga.

My research area is the theory and practice of programming languages.

Currently, I am focusing on incremental computation, using types to guide and automate the generation of programs that respond asympotically faster to changing inputs, and on union, intersection and refinement types to represent and verify diverse program properties. These two directions reinforce each other: advanced type systems make type checking difficult, so these type checkers (and associated technologies like SMT solvers) are an attractive target for incrementalization; on the other hand, generating correct incremental programs requires that we check properties about the relationships between pieces of a computation.

I received my Ph.D. from Carnegie Mellon, where I worked with Frank Pfenning.

For more details, see my CV (last updated April 2020).

Not too long ago, I became a permanent resident of Canada.

  Vancouver trolleybus

Electric trolleybus in Vancouver.

Research list of publications

Some current projects:




Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types was accepted to POPL 2019.

NSERC increased my Discovery award to $33,000/year.

Was awarded a Discovery grant ($26,000/year for 5 years) from NSERC/CRSNG.

2017: Moved to Kingston and joined the School of Computing at Queen's.

2016: Completed a draft on refinement types for incremental computation.

"Extensible datasort refinements" was accepted to ESOP 2017.

"Sums of Uncertainty: Refinements go gradual" was accepted to POPL 2017. My coauthor, Khurram A. Jafery, received a 2017 CRA Outstanding Undergraduate Researcher award.

2015: "Incremental computation with names" appeared at OOPSLA 2015. "Elaborating evaluation-order polymorphism" appeared at ICFP 2015. Completed a draft on bidirectional typechecking for GADTs and a draft on evaluation-order polymorphism.

2014: I moved from Kaiserslautern to Vancouver.

Two papers have been accepted to the Journal of Functional Programming and will appear in 2014: an extended version of my ICFP 2012 paper on intersection and union types, and an extended version of our ICFP 2011 paper on implicit self-adjusting computation.

2013: The paper "Complete and easy bidirectional typechecking for higher-rank polymorphism" was accepted to ICFP 2013, and the final version is on the arXiv.

All papers and publications


Random bits

OS X keyboard layout with some PL-related symbols

Keyboard layout that allows directly typing Greek letters, turnstiles, union, intersection, and other symbols. Install in ~/Library/Keyboard Layouts. Annoyingly, you need to log out and log back in to make the layout available.


A shell script that uses pdflatex to add page numbers to PDFs without them. Note that pdflatex will lose internal hyperlinks, so you probably don't want this on-screen, but it's great for printing.


If you use OS X and prefer spell to ispell, try GNU spell with getline included (OS X does not have getline). You may also need to sudo port install ispell (GNU spell is just a wrapper).


Jana Dunfield
School of Computing
Goodwin Hall, Rm. 557
Queen's University
Kingston, ON  K7L 3N6