Papers
2008
Higher Order Constraint Simplification in a Dependent Type Theory
(Submitted to CSL'08)
[
LaTeX
]
2007
A Hybrid Metalogical Framework
(Thesis Proposal Working Draft)
[
PS
]
2006
Hybridizing a Logical Framework
(HyLo 2006, ©
Elsevier
)
Intuitionistic Letcc via Labelled Deduction
(Unpublished Manuscript)
[
Twelf
]
2004
Redundancy Elimination for LF
(LFM 2004)
[
LaTeX
]
2003
Extending Higher-Order Unification to support Proof Irrelevance
(TPHOLs 2003, ©
Springer-Verlag
)
2002
Higher-Order Pattern Unification and Proof Irrelevance
(TPHOLs 2002 Track B, published in NASA tech report CP-2002-211736)
[
LaTeX
]
Proof Irrelevance and Strict Definitions in a Logical Framework
(Senior Thesis, published as 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
]
2000
Inverting the Cantor-Bendixson Derivative
(Final project for 21-651 Topology, Fall 2000)
[
LaTeX
]
See also my
drafts
.