I am interested in the design of functional programming languages, type systems, and program verification.
Talks I've Given
Designing and Verifying Programs with Formal Specification
Featuring Jacob Leach
In this talk, I will give an overview of Spectacle, a Haskell EDSL for writing formal specifications in the temporal logic of actions, and how specifications written in Spectacle can mechanically verify real-world Haskell programs.haskell edsl specifications spectacle