FOUNDATIONS OF PROGRAMMING LANGUAGES IN COQ
- Academic year
- 2025/2026 Syllabus of previous years
- Official course title
- FOUNDATIONS OF PROGRAMMING LANGUAGES IN COQ
- Course code
- PHD226 (AF:588775 AR:333343)
- Teaching language
- English
- Modality
- On campus classes
- ECTS credits
- 2
- Degree level
- Corso di Dottorato (D.M.226/2021)
- Academic Discipline
- INF/01
- Period
- Annual
- Course year
- 1
- Where
- VENEZIA
- Moodle
- Go to Moodle page
Contribution of the course to the overall degree programme goals
Formal methods are of the fundamental importance for computer scientists, and this PhD-level course aims to provide an introduction to the theory of programming languages.
In particular, the goals of this course are: introduce students to the syntax and semantics of programming languages in Rocq (a proof assistant formerly known as Coq).
In particular, the goals of this course are: introduce students to the syntax and semantics of programming languages in Rocq (a proof assistant formerly known as Coq).
Expected learning outcomes
Attendance and active participation in the course, along with individual study, will enable participants to:
1. Knowledge and Understanding
1.1. gain a foundational understanding of the syntax and semantics of programming languages in Rocq;
2. Ability to Apply Knowledge and Understanding
2.1. be able to model a simple language in Rocq;
2.3. utilize Rocq to demonstrate simple properties of languages and programs.
3. Ability to Judge
3.1. valutare formulazioni alternative di linguaggi di programmazione, le loro proprietà e discuterne vantaggi e svantaggi.
1. Knowledge and Understanding
1.1. gain a foundational understanding of the syntax and semantics of programming languages in Rocq;
2. Ability to Apply Knowledge and Understanding
2.1. be able to model a simple language in Rocq;
2.3. utilize Rocq to demonstrate simple properties of languages and programs.
3. Ability to Judge
3.1. valutare formulazioni alternative di linguaggi di programmazione, le loro proprietà e discuterne vantaggi e svantaggi.
Pre-requirements
Students are required to have a basic knowledge of set theory, logic, and mathematical induction. Additionally, familiarity with at least one functional programming language (such as OCaml, Haskell, Agda, F#, Scala, Lean, etc.) is suggested.
Contents
* Block 1 (1h + 3h lab)
+ Introduction to verified software and motivation
+ (Guided lab) Basics of the Rocq theorem prover
+ (Lab) Q&A; Rocq exercises
* Block 2 (4h + 2h lab)
+ Syntax and semantics of programming languages
+ Examples: imperative, functional and low level
+ (Guided lab) Definition of simple programming languages, various paradigms and styles of semantics
+ Introduction to verified software and motivation
+ (Guided lab) Basics of the Rocq theorem prover
+ (Lab) Q&A; Rocq exercises
* Block 2 (4h + 2h lab)
+ Syntax and semantics of programming languages
+ Examples: imperative, functional and low level
+ (Guided lab) Definition of simple programming languages, various paradigms and styles of semantics
Referral texts
[1] B. C. Pierce et al., "Software foundations, Vol 1: Logical Foundations", https://softwarefoundations.cis.upenn.edu/lf-current/index.html
[2] B. C. Pierce et al., "Software foundations, Vol 2: Programming Language Foundations", https://softwarefoundations.cis.upenn.edu/plf-current/index.html
[2] B. C. Pierce et al., "Software foundations, Vol 2: Programming Language Foundations", https://softwarefoundations.cis.upenn.edu/plf-current/index.html
Assessment methods
Two options, expected amount of work ~4/8h, both to be discussed with the instructor:
* Seminar: organize a 45m/1h seminar on an advanced topic of choice
* Project: develop a non-trivial extension to one of the exercises/topics covered in the course (e.g., additional features on a compiler)
* Seminar: organize a 45m/1h seminar on an advanced topic of choice
* Project: develop a non-trivial extension to one of the exercises/topics covered in the course (e.g., additional features on a compiler)
Type of exam
oral
Grading scale
The exam result can be either "approved" or "not approved". The "approved" result requires:
- sufficient knowledge of the course topics and adequate applied understanding;
- autonomous and coherent capacities for analysis, evaluation, and interpretation;
- appropriate and controlled use of technical terminology;
- clear and well-structured presentation.
- sufficient knowledge of the course topics and adequate applied understanding;
- autonomous and coherent capacities for analysis, evaluation, and interpretation;
- appropriate and controlled use of technical terminology;
- clear and well-structured presentation.
Teaching methods
Classroom-based course supplemented by exercises conducted during laboratory hours (potentially online) to reinforce concepts and encourage discussion among students.
Definitive programme.
Last update of the programme: 17/11/2025