Education

• [Ph.D. [expectedAugust 1998]] Cornell University (Computer Science, minor in Mathematical Logic) Thesis Decidability Extracted: Synthesizing ``correct-by-construction'' decision procedures., under the supervision of Robert Constable, Fred Schneider, and Anil Nerode.
• [M.S.] 1995 Cornell University (Computer Science)
  Awarded upon completion of exam for admission to Ph.D. candidacy.
• [M.S.] 1988 State University of New York at Albany (Computer Science)
• [B.S.] 1984 State University of New York at Albany (Computer Science)

Work Experience

• [1997- now] NASA Ames Research Center, Moffett Field, CA. (Computer Scientist)
  On leave at Cornell to finish Ph.D.
• [1988-1997] NASA Langley Research Center, Hampton, VA. (Computer Scientist)
• [1985-1988] General Electric Corporate Research and Development Center/Infologic Software Inc.,
  Schenectady, N.Y. (VLSI CAD Software Engineer)
• [1983-1985] Phoenix Data Systems, Albany, N.Y., (VLSI CAD Software Engineer)
• [1980-1981] CMT Trade Center, N.Y., N.Y. (Systems Programmer)
• [1979-1980] NPS Automation Services Inc., Secacus, N.J. (CAD Systems Specialist)

To Appear

• [] James L. Caldwell: Classical Propositional Decidability via Nuprl Proof Extraction. TPHOLs'98: The 11th International Conference on Theorem Proving in Higher Order Logics.
• [] James L. Caldwell, Ian Gent and Judith Underwood: Search Algorithms in Type Theory. To Appear in The Journal of Theoretical Computer Science in a special issue devoted to Proof Search in Type-theoretic Languages.

Publications and Reports

• [] James L. Caldwell: Moving Proofs-as-Programs into Practice. In the Proceedings, 12th IEEE International Conference Automated Software Engineering (ASE'97), Incline Village, NV, November 1997.
• [] James L. Caldwell and Judith Underwood: Classical tools for constructive proof search. Proceedings of the CADE-13 Workshop on Proof search in type-theoretic languages, pp.31 - 40. Edited by Didier Galmiche, Rutgers N.J., 30 July 1996.
• [] James L. Caldwell: Formal Methods Technology-Transfer: a View from NASA. Formal Methods in System Design. Volume 12, No. 2, pp. 125 - 137, March 1998. An earlier version appears in the Proceedings of the ERCIM Workshop on Formal Methods for Industrial Critical Systems, pp. 1 - 16, Oxford England. Edited by S. Gnesi and D. Latella. 19 March 1996.
• [] Ricky W. Butler, James L. Caldwell, Victor Carreno, Michael Holloway, Paul Miner and Ben L. Di Vito: NASA Langley's Research and Technology Transfer Program in Formal Methods. In 10th Annual Conference on Computer Assurance (COMPASS 95), Gaithersburg, MD, June 1995.
• [] Ricky W. Butler, James L. Caldwell, and Ben L. Di Vito: Design strategy for a formally verified reliable computing platform. In 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, MD, June 1991.
• [] Ben L. Di Vito,Ricky W. Butler, and James L. Caldwell: High level design proof of a reliable computing platform. In Dependable Computing for Critical Applications 2, Dependable Computing and Fault-Tolerant Systems, pages 279-306. Springer Verlag, 1992. Also presented at 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, AZ, Feb. 18-20, 1991, pp. 124-136.
• [] Paul S. Miner and James L. Caldwell: A HOL theory for voting. In NASA Formal Methods Workshop 1990, pages 442-456, NASA CP-10052, November 1990.
• [] Ben L. Di Vito, Ricky W. Butler, and James L. Caldwell: Formal design and verification of a reliable computing platform for real-time control (Phase 1 results). NASA Technical Memorandum 102716, October 1990.
• [] James L. Caldwell, Ricky W. Butler, and Ben L. Di Vito: Hierarchical approach to specification and verification of fault-tolerant operating systems. In DARPA/Army Workshop on Software Tools for Distributed Intelligent Control Systems, Pacifica, CA., July 1990.

Selected Talks

• []Formal Methods: Industrial Applications from the NASA Portfolio. An invited talk given at Raytheon Systems Canada Ltd., Richmond, British Columbia, 22 May 1998.
• [] Moving Proofs-as-Programs into Practice. A presentation given at the 12th IEEE International Conference Automated Software Engineering (ASE'97), Incline Village, NV, 5 Nov 1997.
• [] Classical tools for constructive proof search. A presentation given at the Workshop on Proof search in type-theoretic languages held in conjunction with CADE-13, Rutgers N.J., 30 July 1996.
• [] A Constructive account of Correct-by-construction. A talk given at NASA Langley Research Center, 26 April 1996.
• [] Formal Methods Technology Transfer: A View From NASA. An invited presentation given at the Laboratory for Foundations of Computer Science at University of Edinburgh,28 March 1996.
• [] Type theory, -calculus, the Curry-Howard Isomorphism and all that. A talk presented at the Formal Methods and Software Engineering Seminar, NASA Langley Research Center, 30 September 1994.
• [] Formal verification of fault-tolerant systems for Hybrid Applications. An invited presentation given at the Hybrid Systems Workshop, Mathematical Sciences Institute, Ithaca, N.Y., June 10-12, 1991.
• [] Close Enough For Government Work: Reflections on Models of Faulty State Machines. Presented at the First NASA Langley Formal Methods Workshop, Langley Research Center, August 1990.

Professional Activities

• [] Invited Reviewer, FormalWARE Project Review, Department of Computer Science, University of British Columbia, Vancouver, Canada, 21 May 1998.
• [] Program Committee, Lfm97, The Fourth NASA LaRC Formal Methods Workshop, Hampton, VA, 1997.
• [] Panel Chair, Researcher Perspectives on Formal Methods. Third NASA LaRC Formal Methods Workshop, Hampton, VA, 1995
• [] Referee: Fourth International Conference on Principles and Practice of Constraint Programming, CP'98; COMPASS 1996; IFIP Working Conference on Dependable Computing for Critical Applications, DCCA-5, 1995; IFIP Working Conference on Dependable Computing for Critical Applications, DCCA-4, 1993; FTCS-19, The Nineteenth International Symposium on Fault Tolerant Computing, 1989.
• [] Session Chair, Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects. Mathematical Sciences Institute, Cornell University, July 1989.

Research Interests

• [] Provably correct approaches to digital design via synthesis and/or transformation based approaches. Verified decision procedures. Theorem proving and application of theorem provers to digital verification. The application of formal methods to fault-tolerant system verification.
  A two page Statement of Research is available.

• About this document ...