编程语言的设计原理


课程信息

上课时间: 每周 周三 10-12节
上课地点: 地学 108
任课教师: 胡振江 教授
赵海燕 副教授
熊英飞 副教授
课程助教: 曾沐焓(邮件:mhzeng@pku.edu.cn

课程通知

作业请用电子方式完成,或者手写之后拍照。每次课的作业在下次课上课前发送到助教的邮箱,邮件标题请以“作业X_学号_姓名”格式书写。

因为新冠疫情的影响,暂定前两周的课通过网络自学的方式完成。课程内容会在上课时间前上线,请大家参照教材和PPT(部分带录音)自学。如果有问题可以随时在微信群里交流。

课程简介

新兴的程序设计语言层出不穷,这些语言是如何设计出来的? 主流语言中不断扩展出新的高级语言特征,这些特征是如何定义的? 为什么说Java语言的设计是有缺陷的?面向对象、函数语言、泛型编程等新型编程模型是否有共通的理论基础? 本课程将揭示这些问题的答案。

近十多年来,编程语言的发展呈现两个趋势:1)从固定少量语言到大量领域特定语言的变化; 2)从简单语言到复杂高级语言。比如,在2013年9月的TIOBE的编程语言排行榜上, C和Java两个占统治地位的语言只能各自占到16%左右的份额, 大量的份额被近年来涌现的新型编程语言比如Javascript, Scala, Erlang, R占据。 同时,更多的新语言还在不断被设计出来。另一方面,大量经典语言也不断扩展, 引入各种高级语言成分。比如Java起初的设计目标为一个简化版的语言, 但最新的Java 8设计中已经包含了泛型、函数式编程、动态性等多种高级特性。在这样的情况下, 掌握设计新的编程语言的能力,已经不仅限前沿科研人员所掌握的高级技能,而是一线软件开发工程师的基本要求 。同时,对语言设计原理的了解和掌握,也有助于更好的理解高级语言中的各种新特性,以更好的使用主流编程语言。

为指导编程语言的设计,研究人员们已经提出了一系列的原理和方法,其中最核心的就是类型理论。 类型声明是现代语言中避免编程错误的一个基本手段,而类型理论解释了一个良好的类型系统应该具有的特征和复杂类型的定义方法。 本课程将围绕类型理论这个核心进行组织,讲授程序设计语言的现代理论。

本课程具有两个特点:1. 严谨性:课程中的概念元素都将有严格的数学定义,可以进行形式演绎和归纳, 而非空泛的概念介绍。2. 操作性:课程中的所有重要概念都将通过课程作业的方式编程实现,使得同学们在动手过程中真正掌握知识。希望通过本课程的学习,使得同学们在编程语言领域拥有扎实的理论功底和实践能力,在产业方面能胜任设计新语言的任务,在学术方面为开展程序语言相关研究打下基础。

参考书目

Types and Programming Languages , Benjamin C. Pierce, The MIT Press, 2002. (教材)

课程讲义和作业

课程日期 讲师 课程章节和讲义 作业
2020/2/19 熊英飞 课程介绍(带录音,3月11日前链接有效)
Untyped Systems
作业1:3.5.16; 安装使用OCaml
2020/2/26 赵海燕 OCaml Overview 作业2:见胶片最后一页
2020/3/4 熊英飞 The Untyped Lambda Calculus
Nameless Representation of Terms
作业3:见胶片最后一页(5.3.6 , 6.2.5)
2020/3/11 熊英飞 Typed Arithmetic Expression
Simply Typed Lambda Calculus
Simply Extensions
课程项目
作业4:见三份胶片的最后一页(8.3.7,9.3.9,11.11.1)
2020/3/18 赵海燕 Reference_part1
Reference_part2
Reference(北大网盘镜像)
作业5:13.3.1, 13.5.2
2020/3/25 熊英飞 In-Class Practice
程序包: problems
作业6:见胶片第一页
2020/4/1 赵海燕 Exception
Subtyping
作业7:14.3.1, 15.3.2, 15.3.6
2020/4/8 各位同学 开题报告和期中测验
2020/4/15 赵海燕 Metatheory of Subtyping_part1
Metatheory of Subtyping_part1
作业8:16.1.2, 16.2.6, 16.3.4
2020/4/22 熊英飞 Case Study: Imperative Objects
Case Study: Featherweight Java
作业9:18.11.1
2020/4/29 赵海燕 In-Class Practice
作业10:18.6.1;18.7.1;17.3.1;17.3.3;19.4.3
2020/5/13 胡振江 Recursive Types
Metatheory of Recursive Types
作业11:见胶片最后一页
2020/5/20 胡振江 Metatheory of Recursive Types
Type Reconstruction
作业12:21.5.2 22.5.5
2020/5/27 胡振江 Universal Types
Existential Types