James Caldwell -- Publications

Publications

Lecture Notes

James Caldwell. Logic and Discrete Mathematics for Computer Scientists 186 pp. + xii, August, 2011. (Draft) [PDF]

Publications and a few Talks

James Caldwell, Ian P. Gent and Peter Nightingale. Generalized Support and Formal Development of Constraint Propagators, AI Communications, pp. vol. 30, No. 5, pp. 325--346, 2017. [pdf]
Hadi Shafei and James L. Caldwell: Bind Induction: Extracting Monadic Programs from Proofs, 21 pp., October 10, 2013 [PDF, Coq Files: epsilon-Monad.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. 12-14 June 2012. [PDF ].
James Caldwell. Teaching natural deduction as a subversive activity , Presented at the Third International Congress on Tools for Teaching Logic, 1-4 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. 24-38, July 14, 2010, Edinburgh, United Kingdom. [PDF ].
Sunil Kothari and James Caldwell: Toward a machine-certified 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 11-12, 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. 57-63, July 21 2008. [PDF]
Roy Dyckhoff and James Caldwell: Proof Extraction from Multi-succedent Intuitionistic Derivations. Presented at the Workshop on Recent Trends in Proof Theory, 9-11 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. 254-263. 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/CP-2008-215309, pp. 33--35, 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.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]
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]
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 (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]
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]
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 Caldwell, Formal Methods Technology-Transfer: a View from NASA, Formal Methods in System Design , Volume 12, Number 2, Pages 125--137, March 1998.
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, 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 CADE-13 Workshop on Proof Search in Type-Theoretic 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. 135-149, 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 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]

Back to Jim's home page.