Lectures: Tu-Th at 11:00PM--12:30PM in CSE 2154.
Instructor, Office Hours: Ranjit Jhala, Tu 12:30-2p or by appt., CSE 3110
Course Description: 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. The last part of the course will look at recent developments and applications, in areas such as memory management and safe, low-level systems programming, analyzing cryptographic protocols, safe execution of untrusted code, and the verification of device drivers, and the analysis of web applications. Students will be evaluated on the basis of 4-6 assignments, each of which will have a written as well as a ``programming" component, a survey project, the aim of which is to allow students to explore a particular topic in detail and a (take-home) final examination.
Prerequisites: Basic Discrete Math, Programming Experience, and, above all, a keenness to learn the material.
Requirements and Grading: