- Ph.D. Cornell University 1998
- M.S. SUNY Albany 1988
- B.S. SUNY Albany 1984
2012-present: Head, Department of Computer Science, University of Wyoming.
2004-present: Associate Professor, Department of Computer Science, University of Wyoming.
2008: Professor (visiting), School of Computer Science, University of St Andrews, UK.
1998-2004: Assistant Professor, Department of Computer Science, University of Wyoming.
1988-1997: Computer Scientist, NASA Langley Research Center, Hampton, VA.
1985-1988: Software Engineer, Infologic at GE Corporate Research and Development, Schenectady, N.Y.
1983-1985: Software Engineer, Phoenix Data Systems, Albany, N.Y.
1980-1981: Systems Programmer, CMT Trade Center, N.Y., N.Y.
Broadly, my research area is the applications of logic and formal
methods in computer science. My research is motivated by the close
connection between mathematical proofs and computer programs, an idea
that is made precise by the Curry-Howard isomorphism. Areas of
specialty include functional programming, constructive logic, type
theory, theorem proving, applications of proofs-as-programs, extraction
of programs from formal proofs. I am also doing joint research with
colleagues in the philosophy department designing logics to model
James Caldwell and Ryan Roan. Type Checking SQL for Secure
Database Access, 2012 Symposium on Trends in Functional Programming (TFP
2012), University of St Andrews, UK. June 12-14, 2012.
James Caldwell. Teaching natural deduction as a subversive
activity , Third International Congress on Tools for Teaching Logic,
June 1-4, 2011,Salamanca, Spain.
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, pp. 24-38, July
14, 2010, Edinburgh, UK.
Sunil Kothari and James Caldwell. A Machine Checked Model of MGU
Axioms, Applications of Finite Maps and Functional Induction, UNIF
2009, the 23nd International Workshop on Unification, August 2, 2009,
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Ã¶ pp.
254-263. University of Athens, June 2008.
James Caldwell & Josef Pohl, Constructive Membership
Predicates as Index Types, Electronic Notes in Theoretical Computer
Science, 174 (7), p.3-16, Jun 2007
Tjark Weber & James Caldwell, Constructively Characterizing
Fold and Unfold, in Logic Based Program Synthesis and Transformation,
LNCS, Vol. 3018, pp. 110 - 127, 2004.