Principles of Programming Languages

Spring 2023

This is an advanced graduate course that discusses programming language reasoning and design. The primary goal of this course is to provide students with a more modern and sophisticated perspective on languages and programming practice.

Potential topics include (but not limited to):

• Functional programming: the connection with logic via Curry-Howard isomorphism.
• Constructive logic: propositional, first-order, and second order.
• Type theory: theory and its applications.
• Program semantics: operational one and type systems.
• Proof theory: including (semi-)automatic theorem proving and practical proof engineering.

Prerequisite: basic discrete mathmatics. Some familarity with functional programming is better, but not required.