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.