CS 292C: Formal Semantics and Type Systems

This course will investigate the formal specification of programming languages, focusing on their semantics (the behavior of a program when it is executed) and type systems (providing a static guarantee about how a well-typed program will behave), and connecting the two via a formal proof of type system soundness (i.e., that the guarantee provided by a type system correctly describes program behavior according to the programming language semantics). We will start by examining some simple semantics and type systems to illustrate the theoretical concepts, then students will define their own projects in which they will extend this simple language to be more expressive in some manner determined by the student and approved by the instructor, while proving that the extensions are sound. Examples of possible extensions include enforcing security properties via secure type systems, verifying program properties via dependent types, enforcing communication protocols via session types, exploring unconventional language abstractions, etc. The projects are expected to include executable implementations of language interpreters and type checkers. Most class lectures will involve students presenting concepts from their projects to the rest of the class.

Recommended textbook: Benjamin Pierce, "Types and Programming Languages"