To Appear

  • Classical Propositional Decidability via Nuprl Proof Extraction : James Caldwell.
    To Appear in TPHOLs'98 The 11th International Conference on Theorem Proving in Higher Order Logics. September 1998.

  • Search Algorithms in Type Theory: James Caldwell, Ian Gent, and Judith Underwood.
    To appear in Theoretical Computer Science Special Issue on Proof Search in Type-theoretic Languages.
    A draft copy dated May 1998 is available here .

    Constructive Logic and Program Extraction

  • Moving Proofs-as-Programs into Practice : James Caldwell: in Proceedings, 12th IEEE International Conference Automated Software Engineering, 1997 Nov 1-5, 1997, IEEE Computer Society.
    In this paper I show how to extract clean recursive programs from inductive proofs. The method relies on the Nuprl set type to hide unwanted computational content and the use of tactics based on induction lemmas having recursion combinators as their extracts.
  • Classical tools for constructive proof search: James Caldwell and Judith Underwood: Proceedings of the CADE-13 Workshop on Proof Search in Type-Theoretic Languages. Edited by Didier Galmiche, Rutgers N.J., 30 July 1996.
    This paper explores the use of programs verified in a classical proof system, PVS in constructive proofs in Nuprl.
  • Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extract: James Caldwell: Unpublished Manuscript.
    This paper describes a formal Nuprl proof of propositional decidability. The Nuprl proofs and definitions can be viewed online as well.
  • A Short Ride Through a Vast Machine: A terse guide to system T++. James Caldwell: Unpublished Manuscript, January 1, 1992.
    This note describes the formal system T++ (an extension of Godel's system T) as presented in Robert Constable's graduate programming languages class at Cornell. It illustrates the propositions-as-types interpretation as justified by the Curry-Howard isomorphism.

    Formal Methods Technology Transfer

  • Formal Methods Technology-Transfer: a View from NASA: James Caldwell: Formal Methods in System Design , Volume 12, Number 2, Pages 125--137, March 1998.
    An earlier version of the paper appeared in the Proceedings of the ERCIM Workshop on Formal Methods for Industrial Critical Systems, Oxford England. Edited by S. Gnesi and D. Latella. 19 March 1996.
  • NASA Langley's Research and Technology Transfer Program in Formal Methods: Ricky Butler, James Caldwell, Victor Carreno, Michael Holloway, Paul Miner; and Ben Di Vito: In 10th Annual Conference on Computer Assurance (COMPASS 95), Gaithersburg, MD, June 1995.

    Formal Methods Applied to Fault-Tolerant Systems

  • High Level Design Proof of a Reliable Computing Platform. Ben Di Vito, Ricky Butler, and James Caldwell: In Dependable Computing for Critical Applications 2, Dependable Computing and Fault-Tolerant Systems, pp. 279-306. Springer Verlag, Wien New York, 1992. Also presented at 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, AZ, Feb. 18-20, 1991, pp. 124-136.
  • Design Strategy for a Formally Verified Reliable Computing Platform. Ricky Butler, James Caldwell, and Ben Di Vito: In 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, MD, June 1991.
  • A HOL theory for voting. Paul Miner and James Caldwell: NASA Langley Formal Methods Workshop , pages 442--456, NASA CP-10052, November 1990.
  • Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 1 Results) Ben Di Vito, Ricky Butler, and James Caldwell: NASA Technical Memorandum 102716, Oct. 1990.
  • Hierarchical approach to specification and verification of fault-tolerant operating systems: James Caldwell, Ricky Butler, and Ben Di Vito: DARPA/Army Workshop on Software Tools for Distributed Intelligent Control Systems, Pacifica, CA., July 1990.

    Back to Jim's home page.