F* Course: Type Systems for Security Verification

Course webpage at Saarland University


  1. Course by Cătălin from Monday, 16 March: Introduction to F* (Board Pictures) (Emacs buffer) (Files from tutorial)
  2. Course by Cătălin from Tuesday, 17 March: F* Basics (Board Pictures)
  3. Course by Cătălin from Wednesday, 18 March: Stateful Verification Basics (Board Pictures) (F* hoare and wlp file) (SF: Hoare logic, decorated programs) (Emacs buffers: hoare)
  4. Course by Cătălin from Thursday, 19 March: Effectful Verification with the Dijkstra monad (Board Pictures) (Files: swap, read)
  5. Course by Niklas from Friday, 20 March: Formalized Metatheory in F*: While and STLC (Board Pictures) (Files: arith.fst, while.fst, stlc.fst)
  6. Course by Cătălin from Monday, 23 March: Formalized Metatheory in F*: LambdaOmega (Board Pictures) (Files: db_subst.fst, stlc_strong...fst, lambda_omega.fst)
  7. Course by Cătălin from Tuesday, 24 March: Metatheory of μF* (Board Pictures) (μF* formalization)
  8. Course by Matteo from Wednesday, 25 March: Cryptographic Protocol Verification
  9. Course by Matteo from Thursday, 26 March: Probabilistic Relational Verification for Cryptographic Implementations


  1. Homework from Monday, 16 March: html, zip (Due: Tuesday, 17 March, 9am) (Solutions)
  2. Homework from Tuesday, 17 March: zip (Due: Wednesday, 18 March, 9am) (Solutions)
  3. Homework from Wednesday, 18 March: zip (Due: Thursday, 19 March, 9am) (Solutions)
  4. Homework from Thursday, 19 March: zip (Due: Friday, 20 March, 9am) (Solutions)
  5. Homework from Friday, 20 March: zip (Due: Monday, 23 March, 9am) (Solutions)
  6. Homework from Monday, 23 March: zip (Due: Tueday, 24 March, 9am) (Solutions)


  1. Hoare logic and weakest precondition calculus formalization, by Simon Forest (ENS Paris) and Enrico Steffinlongo (Ca' Foscari University, Venice)
  2. Normalization proof for CBV STLC, by Yannick Forster, Lukas Krämer, and Franziska Müller (Saarland University)
  3. Certificate chains and zero-knowledge proofs, by Inken Hagestedt and Sebastian Laska (Saarland University)