编程语言的设计原理
课程信息
| 上课时间： | 每周 周三 10-12节 | |
| 上课地点： | 二教 304 | |
| 任课教师： | 胡振江 教授 | |
| 赵海燕 副教授 | ||
| 熊英飞 副教授 | ||
| 课程助教： | 刘鑫远（邮件：liuxinyuan@pku.edu.cn） |
课程通知
作业提交：
纸制版作业，每次课的作业在下次课上课前交给助教。
电子版作业，每次课的作业在下次课上课前发送到助教的邮箱，邮件标题请以“X月X日课作业_学号_姓名”格式书写。
课程简介
新兴的程序设计语言层出不穷，这些语言是如何设计出来的？ 主流语言中不断扩展出新的高级语言特征，这些特征是如何定义的？ 为什么说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. (教材) |
课程讲义和作业
| 课程日期 | 讲师 | 课程章节和讲义 | 作业 |
|---|---|---|---|
| 2019/2/20 | 熊英飞 |
Introduction Untyped Systems |
3.5.16; 安装使用OCaml |
| 2019/2/27 | 赵海燕 | OCaml Overview | 4.2.2 |
| 2019/3/6 | 熊英飞 |
Untyped Lambda Calculus Nameless Representation |
见两份胶片的最后一页，共两题 |
| 2019/3/13 | 熊英飞 |
Typed Arithmetic Expression Simply Typed Lambda Calculus Simply Extensions 课程项目 |
见三份胶片的最后一页，共三题 |
| 2019/3/20 | 熊英飞 |
In-Class Practice |
见胶片最后一页 Ocaml老版本程序包： arith fullsimple fullsimple.match.problem Ocaml 4.06可用的程序包（感谢卢思睿同学）： arith fullsimple fullsimple.match.problem |
| 2019/3/27 | 赵海燕 |
Reference |
13.3.1, 13.5.2 |
| 2019/4/3 | 赵海燕 |
Exception Subtyping |
14.3.1, 15.3.2, 15.3.6 |
| 2019/4/10 | 各位同学 | 开题报告和期中测验 | 无 |
| 2019/4/17 | 赵海燕 |
Metatheory of Subtyping |
16.1.2, 16.2.6, 16.3.4 |
| 2019/4/24 | 胡振江 |
Case Study: Imperative Objects Case Study: Featherweight Java |
18.11.1 |
| 2019/5/8 | 赵海燕 |
In-Class Practice |
18.6.1;18.7.1;17.3.1;17.3.3;19.4.3 |
| 2019/5/15 | 胡振江 |
Recursive Types |
见第20章胶片最后一页 |
| 2019/5/22 | 胡振江 |
Metatheory of Recursive Types Type Reconstruction |
见胶片最后一页 |
| 2019/5/29 | 熊英飞 |
Universal Types Existential Types Bounded Quantification |