Self-Adjusting Computation

Beluga: Programming with Higher-Order Abstract Syntax

Polymorphism, Type Refinements, Intersection and Union Types

Joshua Dunfield	Annotations for intersection typechecking Accepted to ITRS ’12, June 2012, Dubrovnik	Draft paper (PDF)
Joshua Dunfield	Elaborating intersection and union types Draft submitted to ICFP 2012	Draft paper (PDF)
Joshua Dunfield	Untangling typechecking of intersections and unions ITRS ’10, July 2010, Edinburgh; post-proceedings version in EPTCS 45, Jan. 2011	Paper (PDF) Slides
Joshua Dunfield	Greedy bidirectional polymorphism ML ’09, August 2009, Edinburgh	Paper (PDF) Slides
Joshua Dunfield	Bidirectional polymorphism through greed and unions March 2009	Draft paper (PDF)
Joshua Dunfield	Refined typechecking with Stardust PLPV ’07, October 2007, Freiburg	Paper (PDF) Slides
Joshua Dunfield	A unified system of type refinements Doctoral dissertation, August 2007	Thesis (PDF) Slides
Joshua Dunfield	Applying type refinements Student Seminar Series talk, May 2005	Slides
Joshua Dunfield Frank Pfenning	Tridirectional typechecking (extended version) March 2004	Technical report (PDF)
Joshua Dunfield	Unifying principles of type refinements February 2004	Thesis proposal (PDF)
Joshua Dunfield Frank Pfenning	Tridirectional typechecking POPL ’04, January 2004, Venice	Paper (PDF) Slides
Joshua Dunfield Frank Pfenning	Type assignment for intersections and unions in call-by-value languages FOSSACS ’03, April 2003, Warsaw (Springer LNCS 2620)	Paper (PDF) Slides
Joshua Dunfield	Combining two forms of type refinements September 2002	Technical report (PDF)

Color key

BibTeX entries for all the above papers

Compilers

Ancient History

Interactive Program Verification

• Semi-Automatic Verification of Purely Functional Programs (undergraduate thesis, May 2000)
  Note to the people who Google for "functional programs verification" and find this document: While I'm not sure what you're looking for, it's exceedingly unlikely that my undergraduate thesis fits the bill, and you may wish to consider Lem's sign from the "Second Sally of Trurl and Klapaucius", to wit: THINK.