Joshua Dunfield

[photo]    

I'm a Research Associate (non-tenure-track faculty) at the UBC Department of Computer Science in Vancouver. I work on programming languages from a type-systems perspective—from checking program properties with refinement types to incremental computation.

I was previously a researcher in Programming Languages and Verification 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.

I received my Ph.D. from Carnegie Mellon, where I worked with Frank Pfenning on my dissertation on refined type systems for programming languages, which allow programmers to state, and compilers to check, more invariants about programs. For more details, see my CV (last updated August 2015).

Not too long ago, I became a permanent resident of Canada. In July 2015, CIC sent my permanent resident card—just one year after I applied for it. Heckuva job.

  Vancouver trolleybus

Electric trolleybus in Vancouver.

Research list of publications

Current projects:

Teaching

News

August 2015: "Incremental computation with names" passed both phases of reviewing and will appear at OOPSLA 2015.

May 2015: "Elaborating evaluation-order polymorphism" will appear at ICFP 2015.

February 2015: Completed a draft on bidirectional typechecking for GADTs and a draft on evaluation-order polymorphism.

May 2014: I moved from Kaiserslautern to Vancouver.

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.

All papers and publications

Software

Random bits

pdfnumbers

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

spell

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

Contact

Joshua Dunfield
Dept. of Computer Science, UBC
201–2366 Main Mall
Vancouver, BC  V6T 1Z4
Canada

create counter