Program: Advanced
Computational Content of Classical Logic
Reading Material
Lecture Video
The binary example in Scheme
Realizability and Program Extraction
Lecture Video
Denotational Semantics
Lecture Video
Computation and Normalization as Interaction
Lecture Video
Theorem Proving
Lecture Video
Advanced Topics in Type Theory
Lecture Notes 1 ps
| pdf
Lecture 1 Video
Lecture Notes 2 ps
| pdf
Lecture 2 Video
