Constructive Logic and Program Extraction

• James Caldwell & Josef Pohl, Constructive Membership Predicates as Index Types, Electronic Notes in Theoretical Computer Science, 174 (7), p.3-16, Jun 2007 [PDF]
  

  ---

• Tjark Weber & James Caldwell, Constructively Characterizing Fold and Unfold, in Logic Based Program Synthesis and Transformation, LNCS, Vol. 3018, pp. 110 - 127, 2004. [PDF]
  

  ---

• Tjark Weber & James Caldwell, Quicksort via Bird's Tree Fusion Transformation, Formal Digital Libraries Project, May, 2003. [PDF].
  

  ---

• James Caldwell, Extracting General Recursive Program Schemes in Nuprl's Type Theory, in Logic Based Program Synthesis and Transformation, LNCS, vol 2372, pp. 233 - 244, Springer 2002. [PDF].
  

  ---

• James Caldwell, Ian Gent, & Judith Underwood, Search Algorithms in Type Theory, Theoretical Computer Science, Vol. 232, No. 1-2, pp.55-90, February 2000. [PDF].

  ---

• James Caldwell, Intuitionistic Tableau Extracted , in Automated Reasoning with Analytic Tableaux and Related Methods, LNAI vol. 1617, pp. 82-96, 1999, Springer. [PDF]

  ---

• James Caldwell, Classical Propositional Decidability via Nuprl Proof Extraction , in Theorem Proving in Higer Order Logics, LNCS, vol 1479, pp. 105 - 122, Springer 1998.

  ---

• James Caldwell, Decidability Extracted: Synthesizing "Correct-by-Construction" Decision Procedures from Constructive Proofs, Cornell University Ph.D., August 1998 [PDF]

  ---

• James L. Caldwell, Moving Proofs-as-Programs into Practice, in Automated Software Engineering, 1997. Proceedings., 12th IEEE International Conference , pp. 10 - 17, Nov, 1997, IEEE Computer Society. [PDF]

  ---

• James Caldwell & Judith Underwood, Classical tools for constructive proof search, in Proceedings of the CADE-13 Workshop on Proof Search in Type-Theoretic Languages. Edited by Didier Galmiche, Rutgers N.J., 30 July 1996. [PDF]

  ---

• James Caldwell, Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extract,: Unpublished Manuscript, March, 1997. [PDF]

  ---

• James Caldwell, A Short Ride Through a Vast Machine: A terse guide to system T++, Unpublished Manuscript, January 1, 1992.

Digital Mathematics Libraries

• James Caldwell & Christoph Jechlitschek, A Framework for Interactive Sharing and Deductive Searching in Distributed Heterogeneous Collections of Formalized Mathematics, in Emerging Trends: Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, published as a University of Utah, Department of Computer Science Technical Report No. UUCS-05004 , pp. 17-34, 2004. [PDF]

  ---

• James Caldwell & John Cowles, Representing Nuprl Proof Objects in ACL2: toward a proof checker for Nuprl, Presented at Third International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2002) [PDF]

  ---

• Stuart Allen, James Caldwell, & Robert Constable, Interactive Digital Libraries of Formalized Algorithmic Knowledge, in Electronic Proceedings of the First International Workshop on Mathematical Knowledge Management: MKM'2001, RISC, A-4232 Schloss Hagenberg, Austria. September, 2001. [PDF]

Formal Methods Applied to Fault-Tolerant Systems

• Jeffrey Van Baalen, James L. Caldwell, & Shivakant Mishra, Specifying and Checking Fault-tolerant Agent-based Protocols using Maude in Formal Approaches to Agent-Based Systems, LNAI, vol 1871, pp. 180 - 193, Springer 2001. [PDF]

  ---

• Ben Di Vito, Ricky Butler, & James Caldwell, High Level Design Proof of a Reliable Computing Platform, in Dependable Computing for Critical Applications 2, (Dependable Computing and Fault-Tolerant Systems), J. F. Meyer & R. D. Schlichting (Ed.) pp. 279-306. Springer Verlag, Wien New York, Januarary, 1992. ISBN: 0387823301. [PDF]

  ---

• Ricky Butler, James Caldwell, & Ben Di Vito, Design Strategy for a Formally Verified Reliable Computing Platform., in Computer Assurance, 1991. COMPASS '91, 'Systems Integrity, Software Safety and Process Security'. Proceedings of the Sixth Annual Conference on, Gaithersburg, MD, pp. 125-133, IEEE, June 1991.

  ---

• Paul Miner & James Caldwell, A HOL Theory for Voting, in NASA Langley Formal Methods Workshop , pages 442--456, NASA CP-10052, November 1990. [PDF]

  ---

• Ben Di Vito, Ricky Butler, & James Caldwell Formal Design and Verification of a Reliable Computing Platform For Real-Time Control (Phase 1 Results) : NASA Technical Memorandum 102716, 70 pages, Oct. 1990. [PDF]

  ---

• James Caldwell, Ricky Butler, & Ben Di Vito, Hierarchical approach to specification and verification of fault-tolerant operating systems: : DARPA/Army Workshop on Software Tools for Distributed Intelligent Control Systems, Pacifica, CA., July 1990. [PS]

  ---

Formal Methods Technology Transfer

• James Caldwell, Formal Methods Technology-Transfer: a View from NASA, 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 & D. Latella. 19 March 1996.

  ---

• Ricky Butler, James Caldwell, Victor Carreno, Michael Holloway, Paul Miner; & Ben Di Vito, NASA Langley's Research and Technology Transfer Program in Formal Methods, in Computer Assurance, 1995. COMPASS '95. 'Systems Integrity, Software Safety and Process Security'. Proceedings of the Tenth Annual Conference on, Gaithersburg, MD, pp. 135-149, June 1995. [Postscript]

Lecture Notes on Discrete Mathematics

• Notes on Discrete Mathematics for Computer Scientists: James Caldwell, April, 2007. Draft Copy: [PDF]
  Comments are welcome, jlc@cs.uwyo.edu.