dsss17:DeepSpec暑期学校2017的讲义

dsss17讲义资料 SF本地软件副本，在Coq Intensive（Pierce）和“经过验证的功能算法”（Appel）中使用的第1-3卷 CAL的“带有崩溃的认证软件”的材料（Kaashoek / Zeldovich） “语言规范和变量绑定”的Stlc材料（Weirich）Metalib支持Stlc的库 “经过验证的编译器的结构”的编译器材料（Leroy） 用于“使用QuickChick进行基于属性的随机测试”的质量控制材料（Pierce） vminus资料，用于“ Vellvm：验证LLVM”（Zdancewic）ll Vellvm讲座的其他内容