VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Formal Foundations of Programming Languages
Last Updated: 2026-02-05 16:15:28
Abstract
The course covers topics in the theory of programming languages, types, and program verification, and how to construct and validate that theory with machine-checked proofs in the Coq proof assistant.
Objective
Students will learn how to develop machine-checked proofs, how to rigorously define the semantics of a programming language and its type system, and how to analyze and formally establish the guarantees of well-typed programs.
Content
The course will begin with an introduction to machine-checked proofs and the Coq proof assistant. It will introduce operational semantics, type systems, and type soundness proofs, starting with the simply-typed lambda calculus and then continuing with increasingly expressive languages. In the hands-on part of the course, students will carry out these proofs in Coq themselves. If time permits, the course will close with a module on program logics.
Resources
Lecture Notes
Will be made available on the course website.
Literature
Will be announced in the lecture.
General Information
- Language
- English
- Levels
- MSC , WBZ
- Frequency
- Yearly recurring
Examination
- Type
- session examination
- Mode
- written 120 minutes
- Aids
- A single hand-written sheet of A4 paper.
Registration & Places
- Max Places
- 35
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture with exercise | Formal Foundations of Programming Languages |
|
3 h weekly |
| exercise | Formal Foundations of Programming Languages |
|
1 h weekly |