James Caldwell's papers
The papers (and some talks) are listed by research area with the most
recent being at the top of the list.
Constructive Logic, Type Theory and Program Extraction
- 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]
- Roy Dyckhoff and James Caldwell: Proof Extraction from Multi-succedent
Intuitionistic Derivations. Presented at the Workshop on
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]
- 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
- 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]
- 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]
- 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]
Back to Jim's home page.