Faculty of Computer Science · Alexandru Ioan Cuza University of Iași

Foundations of Programming Languages

Course: Dr. Andrei Arusoaie · Labs: Drd. Delia Iustina Grigoriță, Dr. Andrei Arusoaie

Overview

This course is about the foundations of programming languages: the notions from mathematics and logic that let us say precisely what a language construct means, not just how it is written. The aim is to be able to look at a program written in an unfamiliar programing language, either compiler or AI-generated and be able to cope with it.

What we cover

Mathematical background: first-order logic, sets, strings and languages, induction, inference rules and inductive definitions, and writing rigorous proofs
Lean 4, a proof assistant: defining data and functions, and proving their properties with proofs the computer checks for us
Concrete and abstract syntax
Operational semantics: big-step and small-step
Type systems and type soundness (progress & preservation)
Certified compilation
The λ-calculus: untyped, Church encodings, and simply typed

Tools and Resources

Lean 4 — proof assistant and programming language
Course notes and slides (per week, below)
Discord for questions and announcements (link shared in class)

Weekly schedule

Wk	Topic	Materials
1	Introduction	notes slideslab: ro en
2	Preliminaries: ADTs, functions, induction	notes slideslab: ro en
3	Polymorphism, higher-order functions, logic in Lean	notes slideslab: ro en

🔒 The notes, slides and lab PDFs are password-protected. The password is shared with enrolled students in class / on Discord.

Course description (fișa disciplinei): PDF (Română) · PDF (English)

Evaluation (2026)

Continuous assessment, out of 100 points. Passing requires at least 50%.

Component	Points
Test 1 (during semester)	30
Test 2 (during semester)	30
Lab worksheets	10
Final project	30

Resources & bibliography

Course

Practical Foundations of Programming Languages, Robert Harper; Cambridge University Press, 2016. Online book
Software Foundations — Vol 2, Benjamin C. Pierce et al. Online book
Programming Languages: Principles and Paradigms, Maurizio Gabbrielli, Simone Martini; Springer, 2010. Springer link
The Formal Semantics of Programming Languages — An Introduction, Glynn Winskel; MIT Press, 1993. Online book

Lab

Software Foundations — Vol 2, Benjamin C. Pierce et al. Online book
Lean 4 — learning materials. lean-lang.org/learn

People

Dr. Andrei Arusoaie — course and some labs · andrei.arusoaie@uaic.ro
Drd. Delia Iustina Grigorița — labs

Previous years

Earlier editions (under the former course name):

2025–2026 2024–2025 2023 2022