编程语言的设计原理
课程信息
| 上课时间： | 每周 周三 10-12节 | |
| 上课地点： | 三教 205 | |
| 任课教师： | 胡振江 教授 | |
| 赵海燕 副教授 | ||
| 熊英飞 研究员 | ||
| 课程助教： | 周钊平（邮件：zhouzhaoping@pku.edu.cn） |
课程通知
2017年6月1日：下周为项目报告，每组报告18分钟，提问3分钟。请同学们做好准备。
2017年5月4日：下周为上机课，请同学们带笔记本电脑到课堂。
2017年4月26日：今天的作业是16.2.5和16.2.6，请大家互相转告。
2017年4月13日：下周是开题报告，请同学们做好准备。
2017年3月29日：请同学们注意组队的时间节点。
2017年3月23日：下周起课程由赵海燕老师讲授，敬请期待。
2017年3月8日：Lambda演算在Full Beta Reduction下是confluent，具体可以参考Church-Rosser属性，上课传递的信息有误。
2017年3月4日：3月1日的作业在3月15日上课前提交。
作业提交：
纸制版作业，每次课的作业在下次课上课前交给助教。
电子版作业，每次课的作业在下次课上课前发送到助教的邮箱，邮件标题请以“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. (教材) |
课程讲义和作业
| 课程日期 | 讲师 | 课程章节和讲义 | 作业 |
|---|---|---|---|
| 2017/2/24 | 熊英飞 |
Introduction Untyped Systems |
3.5.16; 安装使用OCaml |
| 2017/3/1 | 赵海燕 | OCaml Overview | 见胶片最后一页 |
| 2017/3/8 | 熊英飞 |
Untyped Lambda Calculus Nameless Representation |
见两份胶片的最后一页，共两题 |
| 2017/3/15 | 熊英飞 |
Typed Arithmetic Expression Simply Typed Lambda Calculus Simply Extensions |
见三份胶片的最后一页，共三题 |
| 2017/3/23 | 熊英飞 |
随堂练习 |
见胶片最后一页，参考作业代码包 |
| 2017/3/29 | 赵海燕 |
Reference 课程项目 |
13.1.2, 13.5.8 |
| 2017/4/5 | 赵海燕 | Exception | 14.3.1 |
| 2017/4/12 | 赵海燕 |
Subtyping Algorithmic Subtyping |
15.2.3, 15.2.4, 15.3.2, 16.1.2 |
| 2017/4/19 | 各位同学 | 项目开题和随堂测试 | 无 |
| 2017/4/26 | 熊英飞 | Imperative Objects | 16.2.5, 16.2.6 |
| 2017/5/3 | 熊英飞 |
Featureweight Java Recursive Types |
见两份胶片的最后一页 |
| 2017/5/10 | 赵海燕 | 随堂练习 | 无 |
| 2017/5/17 | 胡振江 | Metatheory of Recursive Types | 21.5.2 |
| 2017/5/24 | 胡振江 | Type Reconstruction | 22.5.5 |
| 2017/5/30 | 胡振江 |
Universal Types Existential Types |
23.5.1, 23.5.2 |