By date (recent first);  By subject

Incremental computation

Matthew A. Hammer
Jana Dunfield
Kyle Headley
Monal Narasimhamurthy
Dimitrios J. Economou 		Fungi: Typed incremental computation with names
July 2018
Draft paper (PDF)
Matthew A. Hammer
Jana Dunfield
Kyle Headley
Nicholas Labich
Jeffrey S. Foster
Michael Hicks
David Van Horn 		Incremental computation with names
OOPSLA ’15, October 2015, Pittsburgh
Paper (PDF)
Yan Chen
Jana Dunfield
Matthew A. Hammer
Umut A. Acar 		Implicit self-adjusting computation for purely functional programs
Journal of Functional Programming, January 2014
Paper (PDF)
Yan Chen
Jana Dunfield
Umut A. Acar 		Type-directed automatic incrementalization
PLDI ’12, June 2012, Beijing
Paper (PDF)
Yan Chen
Jana Dunfield
Matthew A. Hammer
Umut A. Acar 		Implicit self-adjusting computation for purely functional programs
ICFP ’11, September 2011, Tokyo
Paper (PDF) Slides

Bidirectional typechecking, polymorphism, type refinements, intersection and union types

Jana Dunfield Flattening subtyping by eta expansion
December 2024
Draft paper (PDF)
Dimitrios J. Economou
Neel Krishnaswami
Jana Dunfield 		Focusing on Refinement Typing
ACM Transactions on Programming Languages and Systems, June 2023
Paper (PDF)
Khurram A. Jafery
Jana Dunfield 		Sums of Uncertainty: Refinements go gradual
POPL ’17, January 2017, Paris
Paper (PDF) Slides
Jana Dunfield Extensible datasort refinements
ESOP ’17, April 2017, Uppsala
Paper (PDF)
Matthew A. Hammer
Jana Dunfield
Kyle Headley
Monal Narasimhamurthy
Dimitrios J. Economou 		Fungi: Typed incremental computation with names
July 2018
Draft paper (PDF)
Jana Dunfield
Neel Krishnaswami 		Bidirectional typing
ACM Computing Surveys, May 2021
Paper (PDF)
Jana Dunfield
Neel Krishnaswami 		Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
POPL ’19, January 2019, Cascais
Paper (PDF)
Jana Dunfield Elaborating evaluation-order polymorphism
ICFP ’15, August 2015, Vancouver
Paper (PDF) Slides Video (YouTube)
Jana Dunfield Elaborating intersection and union types
Journal of Functional Programming, May 2014
Paper (PDF)
Jana Dunfield
Neel Krishnaswami 		Complete and easy bidirectional typechecking for higher-rank polymorphism
ICFP ’13, September 2013, Boston
Paper (PDF) Slides
Jana Dunfield Elaborating intersection and union types
ICFP ’12, September 2012, Copenhagen
Paper (PDF) Slides Video (YouTube)
Jana Dunfield Annotations for intersection typechecking
ITRS ’12, June 2012, Dubrovnik; post-proceedings version to appear in EPTCS
Paper (PDF) Slides
Jana Dunfield Untangling typechecking of intersections and unions
ITRS ’10, July 2010, Edinburgh; post-proceedings version in EPTCS 45, Jan. 2011
Paper (PDF) Slides
Jana Dunfield Greedy bidirectional polymorphism
ML Workshop, August 2009, Edinburgh
Paper (PDF) Slides
Jana Dunfield Bidirectional polymorphism through greed and unions
March 2009
Draft paper (PDF)
Jana Dunfield Refined typechecking with Stardust
PLPV ’07, October 2007, Freiburg
Paper (PDF) Slides
Jana Dunfield A unified system of type refinements
Doctoral dissertation, August 2007
Thesis (PDF) Slides
Jana Dunfield Applying type refinements
Student Seminar Series talk, May 2005
Slides
Jana Dunfield
Frank Pfenning 		Tridirectional typechecking (extended version)
March 2004
Technical report (PDF)
Jana Dunfield Unifying principles of type refinements
February 2004
Thesis proposal (PDF)
Jana Dunfield
Frank Pfenning 		Tridirectional typechecking
POPL ’04, January 2004, Venice
Paper (PDF) Slides
Jana Dunfield
Frank Pfenning 		Type assignment for intersections and unions in call-by-value languages
FOSSACS ’03, April 2003, Warsaw
Paper (PDF) Slides
Jana Dunfield Combining two forms of type refinements
September 2002
Technical report (PDF)

Beluga: Programming with higher-order abstract syntax

Brigitte Pientka
Jana Dunfield 		Covering all bases: design and implementation of case analysis for contextual objects
October 2010
Draft paper (PDF)
Brigitte Pientka
Jana Dunfield 		Beluga: a framework for programming and reasoning with deductive systems (system description)
IJCAR ’10, July 2010, Edinburgh
Paper (PDF)
Brigitte Pientka
Jana Dunfield 		Programming with proofs and explicit contexts
PPDP ’08, July 2008, Valencia
Paper (PDF) Slides
Jana Dunfield
Brigitte Pientka 		Case analysis of higher-order data
LFMTP ’08, June 2008, Pittsburgh
Paper (PDF) Slides

Colour key

slides video
unrefereed manuscript technical report unrefereed workshop paper
dissertation refereed conference or workshop paper
journal paper

BibTeX entries for all papers

 

Ancient History

Compilers

Jana Dunfield
Aleksey Kliger 		Tail call optimization in SUIF
April 2003
Course project report (PDF)

Interactive Program Verification

 

Jana Dunfield