F* Course: Type Systems for Security Verification
Course webpage at Saarland University
Slides
-
Course by Cătălin from Monday, 16 March: Introduction to F*
(Board Pictures)
(Emacs buffer)
(Files from tutorial)
-
Course by Cătălin from Tuesday, 17 March: F* Basics
(Board Pictures)
-
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)
-
Course by Cătălin from Thursday, 19 March: Effectful Verification with the Dijkstra monad
(Board Pictures)
(Files: swap,
read)
-
Course by Niklas from Friday, 20 March: Formalized Metatheory in F*: While and STLC
(Board Pictures)
(Files: arith.fst,
while.fst,
stlc.fst)
-
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)
-
Course by Cătălin from Tuesday, 24 March: Metatheory of μF*
(Board Pictures)
(μF* formalization)
-
Course by Matteo from Wednesday, 25 March: Cryptographic Protocol Verification
-
Course by Matteo from Thursday, 26 March: Probabilistic Relational Verification for Cryptographic Implementations