Program: Applications

Proof Carrying Code
Lecture Notes 1
Lecture 1 Video
Lecture Notes 2
Lecture 2 Video
Exercizes

Correctness of Hardware Components
Lecture Video

Formalization of Mathematics
Lecture Notes postscript | pdf Lecture Video

Principles and Pragmatics of Subtyping in PVS
Lecture Video

Logical Framework in TWELF
Lecture Video