Academics

  /  

Courses

  /  

Descriptions

COMP_SCI 320: Proving Properties of Programs with Mechanized Logic

VIEW ALL COURSE TIMES AND SESSIONS

Prerequisites

CS 212 and CS 321 or CS MS CS 321 or CS PhDs

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.

• Formerly Comp_Sci 396 - last offer was Spring 2023.
• This course fulfills Technical Elective area.
  

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