Proving Properties of Programs with Mechanized Logic.By the end of this course, expect to have a bet

1 Unit · Graduate

This course will explore the state of the art in how to implement and prove facts about software. We will focus on small, functional programs and expressing properties of them via an (extremely) sophisticated dependent type system.