James Caldwell
Professor Emeritus

Department of Computer Science


    


Work:
+1(307)760-7580


email: jlc@uwyo.edu


Education:
PhD
MS
BS
1998
1988
1984
Cornell University
SUNY Albany
SUNY Albany
Computer Science
Computer Science
Computer Science
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. In exciting developments over the past few years, all these areas are turning out to be important technologies for blockchain. Currently, with my graduate student Kegan McIlwaine, I am designing a smart contract programming language called Faustus. We are implementing a compiiler that targets Marlowe, a Haskell Embedded Domain Specific Language. We are verifying (in Isabelle) the correctness of the compiler with respect to the semantics which are defined in terms of Marlowe's execution semantics.
Current Research Projects : [IOHK] IOHK | Wyoming Advanced Blockchain Research Lab (WABL) co-director with Mike Borowczak
Previous Research Projects: [EPSRC] Proof Theory and Constraint Satisfaction With Ian Gent and Roy Dyckhoff
[NSF] Science of Design: Comprehensibility as a Design Critera with Ruben Gamboa
[NSF] Programming in Constructive Type Theory
Curriculum Vitae: [PDF]
ORCID:
Publications: Available Online
Current Students:
  • Kegan McIlwaine (Ph.D. Student)
    Designing a formally verified compiler for a new smart contract programming language.
  • A. Stone Olguin (M.S. Student)
    Working with the LEAN theorem prover on cyclic groups and cryptography libraries
Former Students:
  • Finley McIlwaine (M.S.) Type CheckingDeclarative Configuration of a Proof-of-Stake Blockchain System
      Haskell Consultant, Well-Typed, Wyoming/London UK
  • Ryan Roan (M.S.) Type Checking SQL
      Senior Software Engineer, Handel Information Technologies Inc., Laramie, WY
  • Sunil Kothari (Ph.D.) Type Inference and Unification: Formal and Informal Proofs in and around Wand's Algorithm
      Senior Researcher at HP Labs, Palo Alto, CA
  • Josef Pohl (Ph.D.) Programming with Evidence
        Director Of Software Development at Skywriter MD
  • Christoph Jechlitschek (M.S.) Sharing Mathematical Knowledge in a Distributed Environment - a P2P Approach.
        Applications Engineer at Intel
  • Tjark Weber (M.S.) Program Transformations in Nuprl.
        Senior Lecturer, Uppsala University.
  • Scott Johnson (M.S.) Program Extraction from Single and Multi-Succedent Intuitionistic Propositional Proofs.
  • Vitali Khaikine (M.S.) Projecting Formal Proofs into XML: Nuprl into HELM
    Research Scientist Department of Engineering, School of Engineering & Technology, Hampton University.