jcreed.org
:
papers
Research Papers
2010
Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy
(with Benjamin Pierce, ICFP'10)
Differential Privacy for Collaborative Security
(with Adam J. Aviv, Daniel Wagner, Andreas Haeberlen, Benjamin C. Pierce, and Jonathan M. Smith, EuroSec'10)
Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic
(with Frank Pfenning, Submitted)
2009
A Hybrid Logical Framework
(PhD Thesis)
Higher-Order Constraint Simplification In Dependent Type Theory
(LFMTP'09)
A Constructive Approach to the Resource Semantics of Substructural Logics
(with Frank Pfenning, manuscript)
2007
A Hybrid Metalogical Framework
(Thesis Proposal Working Draft)
[
PS
]
Intuitionistic Letcc via Labelled Deduction
(With Frank Pfenning, M4M 2007; ©
Elsevier
))
[
Twelf
] [
BibTeX
]
2006
Hybridizing a Logical Framework
(HyLo 2006, ©
Elsevier
)
[
BibTeX
]
2004
Redundancy Elimination for LF
(LFM 2004)
[
LaTeX
] [
BibTeX
]
2003
Extending Higher-Order Unification to support Proof Irrelevance
(TPHOLs 2003, ©
Springer
)
[
BibTeX
]
2002
Higher-Order Pattern Unification and Proof Irrelevance
(TPHOLs 2002 Track B, NASA tech report CP-2002-211736)
[
LaTeX
]
Proof Irrelevance and Strict Definitions in a Logical Framework
(Senior Thesis, CMU tech report CMU-CS-02-153)
[
LaTeX
]
2001
Recursive Datatypes and Diamond Inference
(Final project for 15-816 Linear Logic)
[
LaTeX
]
Formalizing the Construction of Exponentials in an Elementary Topos
(Final project for 15-851 Computation & Deduction, Spring 2001)
[
LaTeX
]
Inverting the Cantor-Bendixson Derivative
(Final project for 21-651 Topology, Fall 2000)
[
LaTeX
]