| 2017 | ESOP | Extensible Datasort Refinements. | Jana Dunfield |
| 2017 | POPL | Sums of uncertainty: refinements go gradual. | Khurram A. Jafery, Jana Dunfield |
| 2015 | ICFP | Elaborating evaluation-order polymorphism. | Jana Dunfield |
| 2015 | OOPSLA | Incremental computation with names. | Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, David Van Horn |
| 2013 | ICFP | Complete and easy bidirectional typechecking for higher-rank polymorphism. | Jana Dunfield, Neelakantan R. Krishnaswami |
| 2012 | ICFP | Elaborating intersection and union types. | Jana Dunfield |
| 2012 | PLDI | Type-directed automatic incrementalization. | Yan Chen, Jana Dunfield, Umut A. Acar |
| 2011 | ICFP | Implicit self-adjusting computation for purely functional programs. | Yan Chen, Jana Dunfield, Matthew A. Hammer, Umut A. Acar |
| 2010 | CADE | Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). | Brigitte Pientka, Jana Dunfield |
| 2008 | PPDP | Programming with proofs and explicit contexts. | Brigitte Pientka, Jana Dunfield |
| 2004 | POPL | Tridirectional typechecking. | Jana Dunfield, Frank Pfenning |
| 2003 | FOSSACS | Type Assignment for Intersections and Unions in Call-by-Value Languages. | Jana Dunfield, Frank Pfenning |