James Caldwell

James Caldwell

Education

• Ph.D. Cornell University 1998
• M.S. SUNY Albany 1988
• B.S. SUNY Albany 1984

Professional Experience

• 2012-present: Head, Department of Computer Science, University of Wyoming.
• 2015-present: Professor, Department of Computer Science, University of Wyoming.
• 2004-2015: 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.

Research Interests
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 beliefs.

Selected Publications

• 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, Montreal, CA
• 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.