软件理论基础与实践 / 2021春

新通知


课程简介

理论计算机科学通常被认为分为A和B两部分(参考ICALP的CFP),A主要是计算相关的理论,包括自动机、算法复杂度等;B主要是软件相关的理论,包括数理逻辑、形式语义、类型系统等。部分国内学者也通俗的将这两部分称为“美式计算机科学”和“欧式计算机科学”。本课程主要讲授软件部分的基础理论,即数理逻辑、形式语义、类型系统的知识。

这些理论知识不仅能丰富和加深我们对软件的理解,也是构造高可信软件的基础。为了确保程序是可信的,一种本质手段是将证明嵌入程序,让计算机自动检查该证明的正确性,确保程序满足需求规约。这样的“带证明程序代码”是目前很多大公司构造高可信关键代码的基础,比如微软、华为都用这种技术构造操作系统内核,而各国的航天航空、高铁等关键代码也常常采用带证明代码的方式构造。该技术也入选了《麻省理工技术评论》2011年选出的年度十大技术。本课程的实践部分将介绍构造这类代码的一个基础编程语言Coq,使得同学们能够掌握构造高可信软件的基本方法,并通过动手实践加深对软件理论的理解。

本课程将首先讲授Coq定理证明工具的使用,然后基于Coq介绍数理逻辑、形式语义、类型系统等相关理论知识,并在Coq中构建一个程序设计语言并证明该语言实现的各种性质。

课程信息

上课时间:双周周二5~6节、每周周五3~4节
上课地点:第三教学楼 504

参考书目

《Software Foundations》,在线书籍

本课程将用到该书籍的第一卷Logic Foundations和第二卷Programming Language Foundations

在线书籍实时更新,本课程本年讲授的时候将采用最新版书籍。

往年课程

  • 2021春

任课教师

胡振江
教授

熊英飞
副教授

课程助教