Kegan McIlwaine Computer Science Ph.D. Defense Announcement

Slides here.

When:

May 1, 2026 at 11:00 a.m. to 1 p.m.

Where:

UWYO Business Building room 208

Zoom: https://uwyo.zoom.us/j/99578050832

Contracts, Simulations, and Sessions: Formal Verification of Compilers, Smart Contracts, and Protocols

Smart contracts are self-enforcing, self-executing protocols governing interactions between several (potentially distrusting) parties. Smart contracts automate the execution of an agreement between participants, typically using the blockchain. The potential for, and the magnitude of, financial losses motivate the application of the most rigorous correctness guarantees to smart contracts, i.e., formal verification. This talk begins with an overview of three results on smart contract semantics, compilation, and transformation verification: a new small-step operational semantics for the Marlowe smart contract programming language, verified against the preexisting evaluation functions; Faustus, a new smart contract programming language that extends Marlowe with parameterized abstractions, an expression language for guarded commands based on the Calculus of Communicating Systems, a type-checker, and a verified compiler; and a formalization of Faustus contracts as concurrent processes with restricted actions, which supports the verification of a smart contract transformation using weak bisimulation. The main focus of this talk is STILL, a standalone tactic-based theorem prover for dependent session types. Session types specify channel communication protocols in the pi-calculus and enjoy a Curry-Howard correspondence with linear logic. Unlike similar provers for linear type theories, STILL allows for delayed linear context partitioning at the tactic level rather than modifying the underlying proof rules. The dependent session type theory implemented in STILL includes a dependent functional layer for specifying the properties of the data being communicated between channels. For this layer, STILL implements a tactic system for the Extended Calculus of Constructions, using techniques inspired by the Rocq theorem prover that improve proof-checking performance. From a proof of protocol validity, STILL extracts a pi-calculus process that is correct by construction with respect to the specified protocol. This talk concludes with verifications of protocols and process extractions for the axiom of choice, natural numbers, and a long-running bit counter, demonstrating the capabilities of STILL and its underlying type theory.