- Curriculum
- Motivation and description
- Course description
- Useful links and Bibliography
- Coq Reference Manual

- Lectures and labs: Andrei Arusoaie
- Contact: andrei.arusoaie@uaic.ro

- Weeks 1 & 2
**Must read:**first chapter in the lecture notes.- Slides
- Lab
- Bibliography: Chapter 13 from [2].

- Week 3
**Must read:**Chapter 2, Sections 2.1 and 2.2 in the lecture notes.- Slides
- Lab
- Bibliography: Chapter Proof
by Induction from [2]
and Chapter
*Inductive Definitions*from [1].

- Week 4
**Must read:**Chapter 2, Sections 2.3, 2.4, and 2.5 in the lecture notes- Slides
- Lab
- Bibliography: Sections Polymorphism and Higher-Order Functions and Logic in Coq from [2].

- Week 5
**Must read:***Chapter 3 - Syntax*from the lecture notes- Slides
- Lab
- Bibliography: Section 4.1 (Chapter 4) from [1].

- Week 6
**Must read:***Chapter 4*,*Section 4.1 - An Evaluator for IMP*from the lecture notes- Slides
- Lab
- Bibliography:
*Volume 1, Section: An Evaluation Function for Imp*from https://softwarefoundations.cis.upenn.edu/lf-current/ImpCEvalFun.html.

- Week 7
**Must read:***Section 4.2*and*Chapter 5*(*Big-step SOS*) from the lecture notes- Slides
- Lab
- Bibliography:
*Volume 1, Section: Evaluation as a Relation*from https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html#lab368.

- Week 8
- Midterm evaluation

- Week 9
**Must read:***Chapter 6*(*Small-step SOS*) from the lecture notes- Slides
- Lab
- Bibliography:
*Volume 2, Small-step Operational Semantics*from https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html.

- Week 10
**Must read:***Chapter 7, Type systems*from the lecture notes- Slides
- Lab
- Bibliography:
*Volume 2, Types*from https://softwarefoundations.cis.upenn.edu/current/plf-current/Types.html.

- Week 11
**Must read:***Chapter 8, Compilation*from the lecture notes- Slides
- Lab
- Bibliography:
*Volume 2, Section: A Small-Step Stack Machine*from https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html#lab179.

- Week 12
- Week 13
**Must read:***Chapter 9, The untyped lambda (λ) calculus*from the lecture notes- Slides
- Lab
- Bibliography:
*Chapter 11 - The Functional Paradigm*from 3.

- Week 14
- Slides
- Lab: final evaluation

- (5 points) RSC_TRANS
- (5 points) RTC_RSC_COINCIDE
- (5 points) bevalR
- (5 points) XtimesYinZ_spec
- (5 points) loop_never_stops
- (5 points) Prove that each big-step SOS transition can be simulated by a number of small-step SOS transitions. You may use/adapt the source code written during the lecture.

[1] *Practical Foundations of Programming Languages*, Robert
Harper; Cambridge University Press, 2016. Online book

[2] *Software Foundations* - Vol 2, Benjamin C. Pierce,
Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael
Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, Brent
Yorgey. Online
book

[3] *Programming Languages: Principles and Paradigms*,
Maurizio Gabbrielli, Simone Martini; Springer-Verlag London Limited,
2010. Springer
link.

[4] *The formal semantics of Programming Languages – An
Introduction*, Glynn Winskell, 1993. The MIT Press, Cambridge,
Massachusetts, ISBN 978-0-262-23169-5. Online
book.