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
Coq Intensive
Day one: Logical Foundations
Chapters
Preface
Basics
Induction
Lists
Poly
Tactics (
Homework:
do the recommended exercises)
Lecture recordings
Video 1
Video 2
Video 3
Video 4
Day two
Chapters
Logic
IndProp
Maps
Lecture recordings
Video 5
Video 6
Video 7
Video 8
Day three
Chapters
Imp
Auto
ProofObjects
Lecture recordings
Video 9
Video 10
Video 11
