Lectures: Tu-Th at 3:30 -- 4:50 Pm in CSE (EBU3B) 2154.
Instructor, Office Hours: Ranjit Jhala, TBD 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. In particular, we will look at operational techniques for formal definition of language features, type systems and type safety properties, polymorphism and subtyping. Students will be evaluated on the basis of homework assignments, each of which will have a written as well as a programming and mechanized theorem proving component. At the end of the class, students will have a very thorough grasp of what it means to formalize the behavior of a computer system and do rigorous proofs about its properties.
Prerequisites: Basic Discrete Math, Programming Experience, and, above all, a keenness to learn the material.
Requirements and Grading: