Courses

  /  

Descriptions

COMP_SCI 396, 496: Proving Properties of Programs with Mechanized Logic

Quarter Offered

Spring : 11-12:20 TuTh ; Findler

Prerequisites

COMP_SCI 212 and COMP_SCI 214; Recommended (but not required): 321 or 325

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://dl.acm.org/citation.cfm?id=2841316 (access via Northwestern's network to download PDF)

COURSE INSTRUCTOR: Prof. Robby Findler