Lectures: Not scheduled yet, please check back soon! (Tomas Petricek and Vít Šefl)
Page in SIS: NPRG085
Grading: Exam
The course will introduce students to theoretical concepts and tools for studying programming languages, including models based on the lambda calculus, operational semantics, and concepts related to type systems. Students will explore the properties of formal models of programming languages (type safety, etc.). The main goal is to prepare students for the study of advanced topics in programming language theory and their practical applications.
This is a new course, jointly taught by Tomas Petricek and Vít Šefl starting in 2026/27. The course is intended as a follow-up to Principles of programming languages (but a prior attendance is not a formal prerequisite). If you are curious how research on programming langauges is done, this is the course for you. More information about the course and the schedule will appear here soon.
Sylabus
The course structure will develop over the semester, but preliminary list of topics that we would like to cover in the course follows. We expect that this will evolve based on what our students will be interested in!
Models of programming languages
- Formal recursive definitions and proofs by induction
- Operational, denotational, and axiomatic semantics
- Inference rules, type systems, and logic
Lambda calculus
- Capture-avoiding substitution, beta reduction, redex
- Normal form, reduction strategies, applicative and normal order
Encoding programming constructs in Lambda calculus
- Recursion, Y combinator, data representation, Church encoding
- Representation of lambda terms, de Bruijn indices
Typed lambda calculus
- Curry-style and Church-style typing
- STLC, System F, Lambda cube, SKI calculus
Operational semantics
- Formal model of an ML-like functional language
- Modeling state, variables, and data structures
Types and programming languages
- Definition of a type system, type safety properties
- Proofs of type safety and related properties
- Hindley-Milner type inference, let polymorphism, bidirectional type systems
- Parametricity (theorems for free!)
Advanced concepts and models
- Formal models of concurrent and distributed computation
- Dependent types, theorem provers, Agda, Idris, LEAN