Beluga: Programming with Higher-Order Abstract Syntax

Polymorphism, Type Refinements, Intersection Types, Union Types

Joshua Dunfield	Greedy bidirectional polymorphism ML '09, August 2009, Edinburgh	Paper Slides
Joshua Dunfield	Bidirectional polymorphism through greed and unions March 2009	Draft paper
Joshua Dunfield	Refined typechecking with Stardust PLPV '07, October 2007, Freiburg	Paper Slides
Joshua Dunfield	A unified system of type refinements Doctoral dissertation, August 2007	Thesis 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
Joshua Dunfield	Unifying principles of type refinements February 2004	Thesis proposal
Joshua Dunfield Frank Pfenning	Tridirectional typechecking POPL '04, January 2004, Venice	Paper 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 Slides
Joshua Dunfield	Combining two forms of type refinements September 2002	Technical report

Color key

BibTeX entries for all the above papers

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.