Advanced Programming Languages (Programming Languages II)

Fall 2026 · School of Electrical and Computer Engineering, National Technical University of Athens

This course studies the formal foundations of programming languages and their use in building reliable software. Topics include operational and axiomatic semantics, compiler correctness, Hoare logic and automated verification, the lambda calculus, type systems and type inference, type classes and monads, program analysis, and memory safety. Lectures and assignments use the Rocq Prover, Haskell, and Rust.

Course Information

Instructor: Zoe Paraskevopoulou
Lectures: Friday 11:45–14:30, Room 8, New ECE Building
Office hours: By appointment (contact the instructor)
Course site: Helios (announcements and assignment submission)
Assignments: Weekly (8–10, tentative), each with a 10-day deadline
Exam: Written final exam, based on the concepts and techniques developed in the assignments. It is designed so that anyone who has engaged substantively with the assignments can do well.
Grading: Assignments 70%, final exam 30%. Passing the course requires a grade of at least 5/10 on the final exam and an overall grade of at least 5/10.
Material: github.com/zoep/PL2 (lecture notes, code, and resources)
Software: The Rocq Prover (version 9.0 or later) and an editor with Rocq support. See the installation instructions in Greek or English.

Sections

The lecture notes are Rocq files meant to be stepped through interactively in your editor. They are updated during the term; the latest versions are always in the course repository.

Section 1

Introduction · The Rocq Proof Assistant I: Functional Programming with Proofs

Course overview and organization. A brief history of the foundations of mathematics and computation, the λ-calculus, the Curry–Howard isomorphism, proof assistants, and Rocq. Functional programming in Rocq: functions and polymorphism, inductive types (booleans, natural numbers, pairs, lists, option), pattern matching, and first proofs by simplification, rewriting, case analysis, and induction.

Slides (PDF) Notes (notes_01_intro.v)

Section 2

The Rocq Proof Assistant II: Logic

Propositions as types: Prop, predicates, and relations. Logical connectives and their proof rules as tactics: implication, universal quantification, True and False, negation, disjunction, conjunction, if and only if, equality, and existential quantification. Inductively defined propositions, proof by contradiction and the excluded middle, and induction on the derivation of a proposition.

Notes (notes_02_logic.v) Practice problems (practice.v) Practice solutions (practice_sol.v)

Section 3

Introduction to Programming Language Semantics · Operational Semantics in Rocq: The Language Imp

Big-step and small-step operational semantics of arithmetic expressions and their equivalence. Proof automation with Ltac: custom tactics and tacticals. The imperative language Imp: states, expressions with variables, commands and their big-step semantics, determinism, a fuel-based interpreter, and a program correctness case study.

Slides (PDF) Notes (notes_03_imp.v) Practice problems and solutions (practice3.zip)

Assignments

Read the instructions at the top of each file before you start. Only the tactics covered in class may be used, and submitted files must compile. Each assignment is available in English and in Greek, and is submitted through Helios.

Assignment 1

Functional Programming and Proofs in Rocq

Booleans; natural numbers; equality of natural numbers; recursive higher-order functions and the Ackermann function. 100 points + 10 bonus points.

assignment1_eng.v (English) assignment1.v (Greek)

Assignment 2

Functions, Binary Numbers, Logic, and Lists

Properties of functions; natural numbers in binary; logic; lists. 100 points + 10 bonus points.

assignment2_eng.v (English) assignment2.v (Greek)

Assignment 3

Operational Semantics of Imp

An Imp program that swaps two variables; correctness of constant folding for Imp; extending Imp with for loops. 100 points + 20 bonus points. The archive also contains imp.v with the Imp definitions from Section 3 and a Makefile; follow the README inside and submit only assignment3.v.

assignment3_eng.zip (English) assignment3.zip (Greek)

References

Benjamin C. Pierce et al., Software Foundations, Volumes I (Logical Foundations) and II (Programming Language Foundations).
Samuel Mimram, Program = Proof.
Benjamin C. Pierce, Types and Programming Languages, MIT Press.

Further reading: PL resources, classic PL papers, and research schools and workshops for students.

Diploma Thesis Topics

If you would like to do your diploma thesis on formal verification, interactive theorem proving, verified compilers, or AI-assisted proof mechanization, see the thesis topics page for the currently available topics. More topics are available on request, and you are welcome to propose your own.