Joshua Dunfield

As of 2017, I am at Queen’s University in Kingston, Canada.
This homepage will not be updated.


I'm a postdoctoral researcher in programming languages at the Max Planck Institute for Software Systems in Kaiserslautern and Saarbrücken. I work on programming languages from a type-systems perspective—from checking program properties with refinement types to incremental computation.

Previously, I was a postdoc with Brigitte Pientka's Computation and Logic Group at McGill University in Montreal, where I worked on Beluga.

I received my Ph.D. from Carnegie Mellon, where I worked with Frank Pfenning on refined type systems for programming languages, which allow programmers to state, and compilers to check, more invariants about programs. Go ahead, read my dissertation. For all the scandalous details about my professional life, see my CV (last updated November 2013).

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

  Vancouver trolleybus

 Electric trolleybus in Vancouver

Research list of publications



May 2014: I have moved to Vancouver. More details soon.

January–March 2014: 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.

June 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.

June-September 2012: The final version of "Elaborating unrestricted intersection and union types" (ICFP 2012) is available, along with a video of the conference talk. I presented some work on type annotations for languages with intersection types at ITRS ’12.

January 2012: Our paper describing an implementation of the theory developed in our ICFP ’11 paper on implicit self-adjusting computation was accepted to PLDI ’12.

January 2011: The final version of a paper at Intersection Types and Related Systems (ITRS 2010) has appeared in EPTCS.

August 2009: I presented Greedy bidirectional polymorphism at the ML Workshop in Edinburgh.

All papers and publications




  • 2013-12-2?–2014-01-0?: North America (tentative)

Random bits

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).