Home

CSE 230: Proofs of Programs, for Programs, by Programs

CSE 230 is an introduction to the Formal Semantics of Programming Languages.

Unlike most engineering artifacts, Programming Languages and Programs are mathematical objects whose properties can be formalized. The goal of this course is to introduce students to fundamental intellectual and mechanical tools required to rigorously analyze Languages and Programs and to expose them to recent developments in and applications of these techniques.

We shall study operational and axiomatic semantics, two different ways of precisely capturing the meaning of programs by characterizing their executions. We will see how the lambda calculus can be used to distill essence of computation into a few powerful constructs. We use that as a launching pad to study expressive type systems useful for for analyzing the behavior of programs at compile-time and then, how to derive expressive program analyses using Abstract Interpretation.

All of the above will be done in a concrete fashion, i.e. by writing programs that define the various kinds of semantics, and writing more programs that correspond to proofs about those objects!