软件科学基础 / 2022春

课程简介

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

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

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

课程信息

上课时间：双周周一7~8节、每周周四5~6节
上课地点：第三教学楼 204

参考书目

《Software Foundations》，在线书籍

• 网址：https://softwarefoundations.cis.upenn.edu/
• 由志愿者维护的中文翻译版：https://coq-zh.github.io/SF-zh/

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

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

往年课程

• 2021春
• 2022春
• 2023春
• 2024春