Marco Patrignani

Programming Languages Semantics 2023-2024

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.

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).

  • Telegram group: link
  • Drive folder with pictures: link

Prerequisites and Interests

Interest in formal languages and formal techniques is important.

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:45 – 10:30 B108
  • Thu 09:30 – 11: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 turn-in must happen through Moodle.

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.

Final exam turn-in must happen through Moodle.

You will then come to the oral exam, to discuss your assignments. The oral exam is a 30 minutes discussion. You should submit your exam 1week before you come do the oral examination.

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 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. intro, ULC syntax, examples
  2. ULC SOS small step CBV, examples
  3. ULC SOS CBN, SOS big step, examples
  4. ULC COS ss CBV, equivalence of SOS and COS (=>)
  5. ULC equivalence of SOS and COS (<=), STLC
  6. STLC sums, pairs, encoding if-then-else, typing
  7. STLC progress
  8. STLC preservation, strong normalisation, logical relation (LR)
  9. STLC LR, semantic typing, fundamental prop, compat for lambda
  10. STLC compatibility lemmas
  11. STLC compatibility lemmas, SF universal types syntax, typing, semantics,
  12. SF existential types & records.
  13. SF new logical relation & compatibility lemmas
  14. Free theorems
  15. Assertions, type safety despite untypability, using the value relation for existentials
  16. Mu types, iso and equi recursive types,
  17. step-indexed LR for mu types
  18. References, usage and typing
  19. Contextual equivalence (CEQ), program contexts
  20. Binary logical relation for CEQ and for parametricity, representation independence
  21. Advanced type systems: Non interference pt1
  22. Advanced type systems: Non interference pt2
  23. Advanced type systems: Speculative semantics and Spectre
  24. Advanced type systems: Dynamic sealing and Encryption
  25. Advanced type systems: Linear typing and Move