Publications
Lecture Notes
 James Caldwell. Logic and Discrete Mathematics for Computer Scientists 186 pp. + xii, August, 2011. (Draft) [PDF]
Publications and a few Talks
 Hadi Shafei and James L. Caldwell: Bind Induction: Extracting Monadic Programs from Proofs, 21 pp., October 10, 2013
[PDF, Coq Files: epsilonMonad.v, decomposition.v ].
 James L. Caldwell: Structural Induction for Functional
Programmers Proceedings of Second Workshop on Trends in Functional Programming in
Education, (TFPIE 2013), May 13, 2013. Provo, Utah. To appear in Electronic Proceedings in Theoretical Computer Science (EPTCS)
[PDF].
 James Caldwell and Ryan Roan. Type Checking SQL for Secure Database Access, 16 pp., Presented at the 2012 Symposium on Trends in Functional Programming (TFP 2012), University of St Andrews, UK. 1214 June 2012. [PDF ].
 James Caldwell, Ian P. Gent and Peter Nightingale. Generalized Support and Formal Development of Constraint Propagators, Unpublished Manuscript, 31 pp., August, 2011. [PDF]
 James Caldwell. Teaching natural deduction as a subversive activity , Presented at the Third International Congress on Tools for Teaching Logic, 14 June, 2011,Salamanca, Spain, 10 pp. [PDF ][Slides]
 Sunil Kothari and James Caldwell. A Machine Checked Model of Idempotent MGU Axioms for a List of Equational Constraints in Electronic Proceedings in Theoretical Computer Science, Vol. 42: Proceedings 24th International Workshop on Unification (UNIF'10), pp. 2438, July 14, 2010, Edinburgh, United Kingdom. [PDF ].
 Sunil Kothari
and James Caldwell: Toward a machinecertified correctness proof of
Wand's type reconstruction algorithm. 4th Informal
ACM SIGPLAN Workshop on Mechanizing Metatheory, 4
September 2009, Edinburgh, Scotland. [Abstract] [Slides]
 Sunil Kothari and James Caldwell. A Machine Checked Model of MGU Axioms, Applications of Finite Maps and Functional Induction
Presented at UNIF 2009, the 23nd International Workshop on Unification, August 2, 2009, Montreal, CA.
[PDF] [Slides]
 James Caldwell, John Cowles and Ruben Gamboa. Enumerating Rationals Without Repetitions.
Presented at ACL2 2009, Eighth International Workshop On
The ACL2 Theorem Prover and Its Applications, May 1112, 2009, Boston, USA. [Abstract] [Slides]
 Nadya Kuzmina, John Paul, Ruben Gamboa and James Caldwell,
Extending Dynamic Constraint Detection with Disjunctive Constraints,
The Sixth International Workshop on Dynamic Analysis (WODA 2008).
pp. 5763, July 21 2008. [PDF]
 Roy Dyckhoff and James Caldwell: Proof Extraction from Multisuccedent
Intuitionistic Derivations. Presented at the Workshop on Recent Trends in
Proof Theory, 911 July 2008, Bern Switzerland. [Slides] [program]
 Sunil Kothari and
James Caldwell, On Extending
Wand's Type Reconstruction Algorithm to Handle Polymorphic Let. Logic and
Theory of Algorithms, Fourth Conference on Computability in Europe,
CiE 2008 , Edited by Arnold Beckmann, Costas Dimitracopoulos, and
Benedikt Löwe. pp. 254263. University of Athens, June 2008 [PDF]
 John Paul, Nadya
Kuzmina, Ruben
Gamboa and James Caldwell, Toward a Formal Evaluation
of Refactorings, The
Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM
2008), NASA/CP2008215309, pp. 3335, May, 2008, Newport News, VA. [PDF]
 James Caldwell & Josef Pohl,
Constructive Membership Predicates as Index Types,
Electronic Notes in Theoretical Computer Science, 174 (7), p.316, 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]
 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. UUCS05004 , pp. 1734, 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 & 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
(ACL22002) [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, A4232 Schloss Hagenberg,
Austria. September, 2001. [PDF]
 Jeffrey Van Baalen, James L. Caldwell, & Shivakant Mishra, Specifying
and Checking Faulttolerant Agentbased Protocols using Maude in
Formal Approaches to AgentBased Systems,
LNAI, vol 1871, pp. 180  193, Springer 2001. [PDF]
 James Caldwell, Ian Gent, & Judith Underwood, Search Algorithms in Type Theory,
Theoretical Computer Science, Vol. 232, No. 12, pp.5590, February
2000. [PDF].
 James Caldwell, Intuitionistic Tableau Extracted , in Automated Reasoning with Analytic Tableaux and Related Methods, LNAI vol. 1617, pp. 8296, 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 "CorrectbyConstruction" Decision Procedures from Constructive Proofs, Cornell University Ph.D., August 1998 [PDF]
 James Caldwell,
Formal Methods TechnologyTransfer: a View from NASA, Formal
Methods in System Design , Volume 12, Number 2, Pages 125137,
March 1998.
 James L. Caldwell, Moving
ProofsasPrograms into Practice, in
Automated Software Engineering, 1997. Proceedings., 12th IEEE
International Conference , pp. 10  17, Nov, 1997, IEEE Computer
Society. [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 & Judith Underwood, Classical tools for constructive
proof search, in Proceedings
of the CADE13 Workshop on Proof Search in TypeTheoretic
Languages. Edited by Didier Galmiche, Rutgers N.J., 30 July
1996. [PDF]
 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. 135149, June 1995. [Postscript]
 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
FaultTolerant Systems), J. F. Meyer & R. D. Schlichting (Ed.)
pp. 279306. 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. 125133, IEEE, June 1991.
 Paul Miner & James Caldwell, A HOL Theory for Voting, in
NASA
Langley Formal Methods Workshop , pages 442456, NASA
CP10052, November 1990. [PDF]

Ben Di Vito, Ricky Butler, & James Caldwell
Formal Design and Verification of a Reliable Computing Platform For RealTime
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 faulttolerant operating
systems: : DARPA/Army Workshop on Software Tools for
Distributed Intelligent Control Systems, Pacifica, CA., July
1990. [PS]
Back to Jim's home page.