Marco Patrignani

Programming Languages Semantics 2022-2023

By prof. Marco Patrignani

General Course Information

How can programming language designers ensure that programmers know exactly what their programs do? Programming language (PL) theory can help answer this and similar questions precisely.

In this course, we study fundamental concepts of PL theory that are essential to the design and specification of programming languages. We will learn how to formalize fundamental concepts such as program syntax, semantics, and type systems, starting from a minimal language (lambda calculus), which we will then extend progressively with more advanced features (algebraic data types, heaps, recursion, and polymorphism) typical of many existing programming languages. Finally, we will see how these PL concepts enable powerful reasoning principles through the use of logical relations, and how to apply them to enforce security (data confidentiality and integrity) through basic language-based information-flow control techniques.

The theoretical lectures on the whiteboard will be accompanied with practical computer sessions on the Agda proof assistant. In these sessions, we will develop interactively, assisted by Agda, computer-certified software artefacts of formal definitions, theorem statements, and proofs. These artefacts are automatically checked for correctness by Agda and therefore give us high-assurance of the validity of the theoretical results.

At the end of the course, students will be able to:

  1. Design expressive programming languages with complex features following established PL methods
  2. Formalize sophisticated type systems that enforce rich program properties and analyse their guarantees using advanced proof techniques.
  3. Reason about program equivalence, correctness, and security formally.

For any question, please contact Marco Patrignani (see mail here).

  • Piazza: TBB

Prerequisites and Interests

Interest in formal languages and formal techniques is important.

Auditing is welcome.

Students that show interest in these topics and want to further their knowledge of them and perform research on these topics are welcome to contact the instructors.

Location and Time Slots

  • Wed 08:30 – 10:30 B108
  • Fri 12:30 – 14:30 A209
  • Office hours: Please drop an email ahead of time if you plan to come.

Evaluation and Grading

The course has a number of intermediate assignments and a final exam. Assignments will help a student consolidate the skills necessary to understand this course as well as prepare them for the final exam. You can collaborate on solutions to exercises together, but you must write your solution individually, in your own words.

  • Assignment 1 [ ] release date: TBD
  • Assignment 2 [ ] release date: TBD
  • Assignment 3 [ ] release date: TBD
  • Assignment 4 [ ] release date: TBD

Assignment turn-in must happen through Gradescope (see link above).

The final exam is a take-home set of exercises analogous to those presented in the assignments. The same collaboration policy as the assignments applies to the exam as well. It will be available on canvas.

  • Exam [ ] release date: TBD

Final exam turn-in must happen through Gradescope (see link above).

Grading:

  • 40% assignments
  • 60% final exam

Course Material

Courses on foundations on PL are widespread, and there are many textbooks and lecture notes out there. However, we focus on quite advanced subjects, and so we recommend the following notes in order to integrate notes taken during class. Please note that the course will indeed follow Dreyer’s notes .

High-level Syllabus

The course is divided in the following parts:

  • Part 0: Typesetting PL notions in LaTeX and Knowing Agda In order to typeset PL notions in LaTeX (akin to those we see in class), please check out this document langref.tex and the related commands file cmds.tex , it should compile to this document .pdf .
  • Part 1: the lambda calculus. Here we’ll see the untyped (ULC) and the simply-typed lambda calculus (STLC), different forms of operational semantics: structural (SOS) and contextual (COS), types such as pairs, products, properties such as progress, preservation, strong normalisation, semantic type soundness.
  • Part 2: System F Here we’ll see System F (SF), the polymorphic lambda calculus with universal and existential types, how to encode them in a semantic model of type soundness (or, logical relation: LR), how to scale the previous properties to this complex setting and how to reason about Parametricity.
  • Part 3: Recursion and Mutable State Here we’ll see how to extend the language with recursive (or \mu) types, their different forms, the semantic model for (now) possibly-diverging computation in the form of Kripke Logical Relations. We’ll also extend the language with a state, so a heap with operations for allocation, reading and writing to it, changing the computation from pure to impure, we will study the semantic model for stateful computation.
  • Part 4: Program equivalence Here we’ll learn how to formalise and reason about the semantics of programs and how to tell when they behave the same, we will see what properties to encode as equivalences and how to develop a semantic model for program equivalence.
  • Part 5: Advanced Type Systems Here we’ll study advanced type systems such as linear types, security types for secure information flow and non-interference, robust-safety typing, multilanguage semantics.

Class Outline

Please note that this is tentative and precise class contents can vary slightly

Class number // class content:

  1. ULC syntax, SOS semantics, examples
  2. ULC small step CBV, CBN, SOS big step
  3. ULC contextual semantics, equivalence of SOS and COS
  4. STLC sums, pairs, encoding if-then-else, typing
  5. STLC progress and preservation, strong normalisation,
  6. logical relation (LR), semantic typing, fundamental prop
  7. STLC compatibility lemmas.
  8. SF: universal types syntax, typing, semantics, existential types & records.
  9. SF new logical relation & compatibility lemmas
  10. Free theorems
  11. Assertions, type safety despite untypability, using the value relation for existentials
  12. Mu types, iso and equi recursive types, step-indexed LR for mu types
  13. References, usage and typing
  14. Kripke worlds
  15. LR with references
  16. Advanced type systems: Non interference pt1
  17. Advanced type systems: Non interference pt2
  18. Contextual equivalence (CEQ), program contexts
  19. Binary logical relation for CEQ and for parametricity, representation independence
  20. Advanced type systems: speculative semantics and spectre
  21. Advanced type systems: linear typing
  22. ..
  23. ..
  24. ..