Toggle navigation
Summer School
Logistics
Installation
Schedule
Lectures
Coq Intensive
Verified functional algorithms
Program-specific proof automation
Certifying software with crashes
The structure of a verified compiler
Property-based random testing with QuickChick
CertiKOS: Certified kit operating systems
Language specification and variable binding
Vellvm: Verifying the LLVM
YouTube channel
DeepSpec Summer School, July 13-28, 2017
Language specification and variable binding
Stephanie Weirich
Lecture one: Locally nameless representation
Material
Stlc/Lec1.v
Stlc/Definitions.v
Lecture recordings
Video 1
Lecture two: Reasoning about LN, nominal representation
Material
Stlc/Lec2.v
Stlc/Lemmas.v
Stlc/Nominal.v
Lecture recordings
Video 2
Lecture three: Connecting Nominal and LN
Material
Stlc/Connect.v
Lecture recordings
Video 3
