More work available on the drafts page.

2009
Higher-Order Constraint Simplification In Dependent Type Theory
(LFMTP'09)
A Constructive Approach to the Resource Semantics of Substructural Logics (Submitted)
2007
A Hybrid Metalogical Framework(Thesis Proposal Working Draft)
Intuitionistic Letcc via Labelled Deduction[PS] (With Frank Pfenning, M4M 2007;
© Elsevier)
[Twelf] @inproceedings{reed-m4m2007, title = {Intuitionistic Letcc via Labelled Deduction}, author = {Jason Reed and Frank Pfenning}, booktitle = {Proceedings of the 5th Workshop on Methods for Modalities (M4M5)}, year = {2007}, editor = {C. Areces and S. Demri} } 2006
Hybridizing a Logical Framework(HyLo 2006, © Elsevier)
@article{reed2006-hybridlf, author = {Jason Reed}, title = {Hybridizing a Logical Framework}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {174}, number = {6}, year = {2006}, pages = {135-148}, } 2004
Redundancy Elimination for LF(LFM 2004)
[LaTeX] @article{reed2004-redundelim, author = {Jason Reed}, title = {Redundancy Elimination for LF}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {199}, year = {2008}, pages = {89-106}, } 2003
Extending Higher-Order Unification to support Proof Irrelevance(TPHOLs 2003, © Springer-Verlag)
@inproceedings{reed-tphols2003, author = {Jason Reed}, editor = {David A. Basin and Burkhart Wolff}, title = {Extending Higher-Order Unification to Support Proof Irrelevance}, booktitle = {Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2758}, year = {2003}, } 2002
Higher-Order Pattern Unification and Proof Irrelevance(TPHOLs 2002 Track B, published in NASA tech report CP-2002-211736)
Proof Irrelevance and Strict Definitions in a Logical Framework[LaTeX] (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)
Formalizing the Construction of Exponentials in an Elementary Topos[LaTeX] (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] |