Research Papers

2010

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]