The program consists of 80-minute lectures.
Nada Amin — Harvard University
Metaprogramming
Lecture 1 video part 1 | part 2 | part 3 | notes
Valeria De Paiva — Topos Institute
Lambda-Calculi for Logics
My preliminary slides:
Lecture 1,
Lectures 2 & 3
Before the first lecture, please fill out this
short homework.
Lecture 1 video part 1 | part 2 | part 3 | notes
Kathleen Fisher — DARPA
Formal Methods for National Security
Limin Jia — Carnegie Mellon University
Information Flow Type Systems
Lecture 1 video part 1 | part 2 | part 3 | notes
Kathryn S McKinley — Google
Better Computing Culture with a Research Mindset = More Innovation
Anja Petković Komel — TU Wien / Argot Collective
Introduction to Type Theories
My lectures are loosely based on the Introduction to Martin-Löf Type Theory in Egbert Rijke's book. We will apply those principles using the Rocq Theorem Prover with VS Code, but Rocq ships with RocqIDE, so also you can use emacs, vim or RocqIDE as editors.
MLTT | Identity Type Two-sided MLTT | Rcoq Intro
Lecture 1 part 1 | part 2 | part 3 | slides | notes
Lecture 2 video part 1 | part 2 | part 3
Lecture 3 video part 1 | part 2 | part 3 | notes
Lecture 4 video part 1 | part 2 | part 3
Lecture 5 video part 1 | part 2 | part 3 | Rcoq Examples
Brigitte Pientka — McGill University
Introduction to Logical Foundations
(aka the beauty of the Curry-Howard Isomorphism at play)
Introduction Logical Foundations of Types and Programming Language
Lecture 1 video part 1 | part 2 | part 3 | notes
Lecture 2 video part 1 | part 2 | part 3 | notes
Lecture 3 video part 1 | part 2 | part 3 |
Emina Torlak — Amazon Web Services
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
The instructions for installing Cedar are here. For the lectures, you should also clone this repo, as it contains the sample code we will be using. The easiest way to edit code in Cedar is through VSCode with the "Cedar" extension.
