Jacob Leach
Expert Overview
Things I'm Doing
Talks I've Given
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