/dsss17

Lecture material for DeepSpec Summer School 2017

Primary LanguageCoq

dsss17 lecture materials

SF local copy of Software Foundations, volumes 1-3 used in Coq Intensive (Pierce) and "Verified functional algorithms" (Appel)

CAL materials for "Certifying software with crashes" (Kaashoek / Zeldovich)

Stlc materials for "Language specification and variable binding" (Weirich) Metalib support library for Stlc

compiler materials for "The structure of a verified compiler" (Leroy)

qc materials for "Property-based random testing with QuickChick" (Pierce)

vminus materials for "Vellvm: Verifying the LLVM" (Zdancewic) ll extra bits for Vellvm lectures