Extending Higher-Order Unification to Support Proof Irrelevance. - Jason Reed 001 (TPHOLs, 2003)

Redundancy Elimination for LF. - Jason Reed 001 (LFM@IJCAR, 2004)

Hybridizing a Logical Framework. - Jason Reed 001 (HyLo@FLoC, 2006)

Intuitionistic Letcc via Labelled Deduction. - Jason Reed 001; Frank Pfenning (M4M, 2007)

Higher-order constraint simplification in dependent type theory. - Jason Reed 001 (LFMTP, 2009)

Differential privacy for collaborative security. - Jason Reed 001; Adam J. Aviv; Daniel Wagner 001; Andreas Haeberlen; Benjamin C. Pierce; Jonathan M. Smith (EUROSEC, 2010)

Distance makes the types grow stronger: a calculus for differential privacy. - Jason Reed 001; Benjamin C. Pierce (ICFP, 2010)