VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.

263-2520-00L 7 Credits MSC , WBZ D-INFK
You're viewing possible stale or outdated data. Please check the latest semester for more up-to-date information.

Formal Foundations of Programming Languages

Lecturers & Examiners: Prof. Dr. Ralf Jung
VVZ CR 4.7

Last Updated: 2026-06-01 11:30:46

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 proceed in two parallel tracks: - The theory track (2V) will introduce operational semantics, type systems, and type soundness proofs, starting with the simply-typed lambda calculus and then continuing with increasingly expressive languages. - The Coq track (2G) will begin with an introduction to machine-checked proofs and the Coq proof assistant. Afterwards we will mechanize the theory developed in the first track. This is the hands-on part of the course; students will carry out these proofs in Coq themselves with instructions from the lecturer.

Resources

Lecture Notes

Will be made available on the course website.

Literature

Will be announced in the lecture.

Learning Materials (Links)

General Information

Language
English
Levels
MSC , WBZ
Frequency
Yearly recurring

Examination

Type
session examination
Mode
written 180 minutes
Aids
A single two-sided sheet of A4 paper, either hand-written or hand-drawn on a screen and then printed.
In the first half of the course, there will be minitests in the exercise group that can be used to earn a grade bonus.In the second half of the course, there will be Coq projects implemented in small groups, which will account for 20% of the grade.

Registration & Places

Max Places
50
Priority: Registration for the course unit is until 29.09.2025 only possible for the primary target group

Course Components

Type Title Time & Place Hours
lecture Formal Foundations of Programming Languages
  • Tue 16:15-18:00 (HG D 3.2)
2 h weekly
exercise Formal Foundations of Programming Languages
  • Wed 12:15-13:00 (CHN F 42)
1 h weekly
practical/laboratory course Formal Foundations of Programming Languages
  • Thu 14:15-16:00 (CHN F 42)
2 h weekly
independent project Formal Foundations of Programming Languages No time listed 1 h weekly

Offered In