Academics

  /  

Courses

  /  

Descriptions

COMP_SCI 396: Proving Properties of Programs with Mechanized Logic

VIEW ALL COURSE TIMES AND SESSIONS

Prerequisites

CS 212 and CS 321

Description

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.

By the end of this course, expect to have a better understanding of how to think about properties of programs, how to write code that demonstrates that those properties are true, and some experience programming in Agda.

COURSE TEXT: Verified Functional Programming in Agda, by Aaron Stump: https://doi.org/10.1145/2841316 (access via Northwestern's network to download PDF)

COURSE INSTRUCTOR: Prof. Robby Findler