Education: 

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 CurryHoward isomorphism. Areas of
specialty include functional programming, constructive logic, type
theory, theorem proving, applications of proofsasprograms,
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) codirector 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 ProofofStake Blockchain System
Haskell Consultant, WellTyped, 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
MultiSuccedent 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.
