CIS 7000-01 Fall 2025
What makes a programming language useful, expressive, safe, or even elegant? How can we evaluate the features of modern programming languages and understand what they can do and how they relate? This course takes a mathematical approach to understanding programming language designs, focusing on their dynamic semantics and static type systems. We’ll rigorously define what programs mean using operational, denotational, and relational semantics, then dive into the expressive power of type theories to provide an abstract view of computation.
Instructor: Stephanie Weirich
Meeting Times: MW 1:45pm-3:14pm (9/03 to 12/8)
Location: 3401 Walnut, 401B
Office Hours: Mondays after class in Levine 510 (starting 9/08)
Prerequisites: We will start from the beginning, so there are no real prerequisites. However, we will move quickly, so even if you have seen some of this before, we will get to new stuff soon. Familiarity with basic functional programming (e.g. OCaml, Haskell or Rocq) is highly recommended. You should be comfortable programming with first-class functions and inductive/algebraic datatypes. CIS 5000 is recommended, especially familiarity with the basics of the untyped and simply-typed lambda calculus.