- PhD Student
I am broadly interested in formal specification and verification of software, in particular of smart contracts. My research focuses on rigorous specification formation, especially relating to blockchain- and cryptocurrency-related phenomena.
I'm tangientially interested in scalability/concurrency, automated market design, business models for the blockchain, etc. These topics can fall within the domain of specification formation in that if one is to build verified software to accomplish these tasks, one must be able to rigorously define desired properties. Often, desired properties are high-level and can thus be difficult to describe rigorously in a formal proof system.
Finally, I am interested in type theory, in particular homotopy type theory, both as it relates to software specification and verification as well as for its own sake.
Part of my work is with the Cambridge Centre for Carbon Credits which focuses on tokenized carbon credits on the blockchain, and verification of the smart contracts corresponding to the tokens and on-chain secondary markets.
