Publications

Journal

James Caldwell and Josef Pohl, Constructive Membership Predicates as Index Types. Electronic Notes in Theoretical Computer Science, Vol. 174, No. 7, pp 3- 16, June 2007. (PDF)

Technical Reports

Monadic Programs Through Program Extraction -- A description of Nuprl monad libraries and code extraction. 2008 ( PDF )


Constructive Membership and Indexes in Trees -- Programming in Nuprl. 2007 ( PDF )


Trees in Constructive Type Theory -- Proofs and formalizations of trees. 2006 ( PDF )