Marco Patrignani

CS358 2020-2021

CS358: PROGRAMMING LANGUAGE FOUNDATIONS

By profs. Marco Patrignani and Marco Vassena

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 both with pen and paper, and with the Agda proof assistant.

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

Prerequisites and Interests

Interest in formal languages and formal techniques is important.
We’ll assume no prior deep knowledge of formal languages and mechanisation. Having attended cs143, or cs242 (2018-2020 edition) or cs350 will provide a bit of background.

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 (all times are in Pacific)

  • Time slot:
    T-TH, 10:30-11:50
  • Location: Zoom :
    https://stanford.zoom.us/j/98488619225
  • Office hours:
    Friday afternoon 10-12, but other slots can be opened if needed.
    Please drop an email ahead of time if you plan to come.
  • Teaching Assistant: TBD

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.

Assignments will be available typically one week in advance before they are due, they are available on canvas (same link as above: https://canvas.stanford.edu/courses/130129/). Typically, they are due on Monday midnight, and they’ll be available the Tuesday before. Please check them out before class and report possible elements of confusion.

  • Assignment 1 [ ] release date: week 2, due date: week 3
  • Assignment 2 [ ] release date: week 3, due date: week 4
  • Assignment 3 [ ] release date: week 4, due date: week 5
  • Assignment 4 [ ] release date: week 5, due date: week 6
  • Assignment 5 [ ] release date: week 6, due date: week 7
  • Assignment 6 [ ] release date: week 7, due date: week 8
  • Assignment 7 [ ] release date: week 8, due date: week 9

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: week 8, due date: week 10

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

Grading: 70% assignments 30% 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 .
    To install Agda, see the piazza post by Marco Vassena.

We will have a preliminary session related to setting up Agda at the beginning of the second week, details on piazza.

  • Part 1: the lambda calculus. Here we’ll see the untyped and the simply-typed lambda calculus, different forms of operational semantics: structural and contextual, 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, the polymorphic lambda calculus with universal and existential types, how to encode them in a semantic model of type soundness, 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: Mechanisation in Agda This part will run alongside the previous ones. Here we’ll learn how to mechanise the languages, typing and operational semantics seen in the other parts. We’ll learn how to prove properties about those languages using Agda and we’ll formalise an advanced type system for reasoning about security for secure information flow and non-interference.

Class Outline

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

The screenshots of each lecture are collected on a google drive folder whose link is on piazza.

  • 12 jan (Patrignani)
    ULC syntax, SOS semantics, small step CBV, CBN
  • 14 jan (Patrignani)
    ULC SOS big step, contextual semantics (COS), equivalence of SOS and COS
  • 19 jan (Vassena)
    Mechanisation of ULC in Agda
  • 21 jan (Patrignani)
    STLC sums, pairs, encoding if-then-else, typing
  • 26 jan (Patrignani)
    STLC progress and preservation, strong normalisation, logical relation (LR), semantic typing, fundamental prop
  • 28 jan (Vassena)
    Mechanisation of STLC in Agda
  • 2 feb (Patrignani)
    STLC compatibility lemmas
  • 4 feb (Vassena)
    Mechanisation of LR in Agda
  • 9 feb (Patrignani)
    SF: universal types syntax, typing, semantics, existential types & records
  • 11 feb (Vassena)
    Mechanisation of records and subtyping
  • 16 feb (Patrignani)
    SF new logical relation & compatibility lemmas
  • 18 feb (Patrignani)
    Free theorems
  • 23 feb (Patrignani)
    Mu types, iso and equi recursive types, step-indexed LR for mu types
  • 25 feb (Patrignani)
    References, usage and typing, Kripke worlds
  • 2 mar (Vassena)
    Mechanisation of mu types and of references in Agda
  • 4 mar (Vassena)
    Mechanisation of the security type system in Agda
  • 9 mar (Vassena)
    Mechanisation of the security type system in Agda
  • 11 mar (Vassena)
    Mechanisation of non-interference in Agda
  • 16 mar (Patrignani)
    Contextual equivalence (CEQ), program contexts
  • 18 mar (Patrignani)
    Binary logical relation for CEQ and for parametricity, representation independence