Lectures are every week on Thursday, 14:00 - 16:00 live. Class will usually include a 15 mins break. (We start at 14:15).

  • Lecture 1: January 11, 
    Topics: λ-calculus: syntax, evaluation judgment, type system, type-preservation and progress; security lattice for confidentiality and integrity, simple & labeled types and λSFG type system, L-equivalence for labeled and simple types, non-interference theorem.
  • Lecture 2: January 25, 
    Topics: λ-calculus with store and references: syntax, evaluation and type system; implicit flows and program-counter label, λSFG typing rules for references.
  • Lecture 3: January 1, 
    Topics: λSFG partitioned store, label-annotated syntax, L-equivalence for references, labeled stores and store maps; properties of L-equivalence (reflexivity, symmetricity, transitivity, store square lemma) proof technique for termination-insensitive non-interference: store containment and L-equivalence preservation lemmas.
  • Lecture 4: February 8, 
    Topics: Coarse grained IFC, labeled values and MAC security monad, λSCG syntax (thunks return, bind, label, unlabel), evaluation (pure, forcing, thunk semantics), type system (no write-down & no read-up rules). Nested computations (toLabeled). Flexible manipulation of labeled values (fmap)., Possibly: Dynamic information flow control

Q&A Session (Mon 16h-18h (sharp))

The Q&A session runs only on Zoom (link here or on the main page). 

  • Q&A 1: 22 January
  • Q&A 2: 29 January
  • Q&A 3: 5 February
  • Q&A 4: 12 February

We will answer questions that pop up on Askbot (see the menu of the course page), even those that appear in anonymous form.
Participation is strongly recommendedDO ask your questions on Askbot: no questions (up until the Q&A session) means no Q&A.

Class Material and Recordings

We will use the lecture notes available in the material section.

Recordings for lectures and Q&A can be found in the materials section
Recordings from previous courses can be found here.

Additional reading material can be found below:



Assignments must be solved, written and submitted individually. You are allowed to discuss the problems with other classmates, but you must not share any solution in written form. Write the answers in English; be clear, precise, and formal. It is recommended to write the answers in LaTeX. Handwritten answers are also acceptable as long as they are legible. Submit your solution in PDF format on CMS (not by email).

Assignments will appear in the course material.

  • Assignment 1 Deadline (January 25th)
  • Assignment 2 Deadline (February 1st)
  • Assignment 3 Deadline (February 8th)

Solutions will appear in the course materials ~1week after deadline.



The oral exam is about 30 minutes long and will take place on Monday February 19th
Location: Live. Room will be announced.

The exam covers the content of the 4 lectures on IFC (see syllabus above). During the exam, you will answer questions about evaluation and typing rules, theorem definitions and proofs, as well as solve small problems similar to those in the exercise sheets. Your grade will be determined based on three criteria: correctness of the answers, clarity of the explanations, and degree of independence in answering the questions.


Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.