本课程为北京大学数学科学学院研本合上课程。

时间：周一3-4节（单），周四3-4节。

地点：三教108。

答疑：双周一10:00-11:00，理科一号楼1382。

课程内容：本课程主要讲授程序设计语言的基本概念和原理，包括程序设计语言的语法和语义描述，词法和语法分析，各种常见语言结构的设计问题和不同语言在语言结构上的设计选择，以及程序设计语言中常见的面向对象、并发、异常处理等机制，并对函数式程序设计语言和逻辑程序设计语言进行讨论。

教材及参考书目：

[1] Robert W. Sebesta. Concepts of Programming Languages. 12th edition, Pearson Education, 2019 (影印版，机械工业出版社，2021).

[2] Kenneth C. Louden, Programming Languages: Principles and Practice (影印版，电子工业出版社，2003).

[3] Ravi Sethi, Programming Languages, Concepts & Constructs，Adison-Wesley，1997 (中译本（裘宗燕等译）及影印本，机械工业出版社，2002).

[4] Glynn Winskel. The Formal Semantics of Programming Languages An Introduction. The MIT Press, 1993.

[5] Seth D. Bergmann. Compiler Design: Theory, Tools and Examples. Rowan University, 2017.

[6] Timothy C. Lethbridge and Robert Laganière. Object-Oriented Software Engineering: Practical Software Development using UML and Java, 2nd edition. McGraw-Hill Education, 2005.

成绩判定：

参加课程学习的每位同学需从Proceedings of POPL 2022或Proceedings of PLDI 2022中任选一篇论文做一次报告，并选择一个课题进行研究，完成一篇课程论文（中英文皆可，中文不少于软件学报格式10页，英文不少于LNCS格式15页），论文课题可从下面建议课题中选择其一，也可根据自己的研究方向自选课题（自选课题需符合本课程宗旨并经与任课教师讨论取得同意，如自选课题，请写一个简短的研究建议，说明所选课题的重要性及与本课程的相关性，通过邮件发送给我，合理的题目都可以通过确认）。

本课程期末成绩将基于平时作业（30%）、前沿论文报告水平（20%）和课程论文（50%）综合评定。平时作业中部分标*的题目为选做内容，选做内容不在计算成绩范围之内，但提交同学最后选做题目所得分数会作为Bonus加到期末成绩之上，加分后的分数上限为100（例如某位同学A前面三部分所得分数合计为85，选做题目得分为5分，则最后总成绩为90，同学B前面三部分所得分数合计为98，选做题目得分为10分，则最后总成绩为100。）。

重要日期（deadline）：

    平时作业提交（教学网）：见课程日程安排。

    确定报告题目及课程论文所选课题（给我发email）：3月31日。

    课程论文提交（教学网）：6月8日。

课程论文可选课题：

    1. Python和C++的面向对象模型研究（也可选择其他两种面向对象的程序设计语言，将两种语言的面向对象模型进行比较，关注语言的继承机制，讨论动态类型的面向对象语言的优势和劣势。）（独立完成）

    2. Java的并行机制、功能和问题（讨论Java的基本并行功能，以及Java中的并行支持库，也可选择其他提供并行机制的程序设计语言进行研究。）（独立完成）

    3. 智能合约编程语言的并行问题（现有的智能合约编程语言如Solidity、Move、Cadence、Liquid等均不能支持并行编程模型，可能原因是什么？会导致什么问题？有什么可能的解决方法？）（独立或合作完成，合作者不超过2人）

    4. Solidity的安全性：设计和问题（研究智能合约编程语言Solidity的安全性机制，语言允许合约做哪些事情？有什么合约需要的特征但由于安全问题语言中未能提供？语言中有什么样的安全漏洞？可以如何解决？）（独立或合作完成，合作者不超过2人）

    5. 智能合约规约语言设计（参考PRISM、Event-B、Mediator等语言，设计一种针对智能合约的形式化规约语言，可采用基于组件的方式构造智能合约的规约，通过该语言对智能合约的重要行为性质进行描述，并给出其严格的语义定义。）（独立或合作完成，合作者不超过3人）

课程日程安排（随课程进度更新）：

序号 课程内容 作业（标*为选做内容）
Lecture 1
Introduction

2月26日前提交本次作业。

1. 如果你支持在所有程序设计领域使用同一种语言，说明支持的理由。

2. 如果你反对在所有程序设计领域使用同一种语言，说明反对的理由。

3. 很多语言区分用户定义名字里头的字母大小写，这个设计有什么优点和缺点？

4*. 阅读《Concepts of Programming Languages》第2章，写一篇不少于2页的简单文献报告，介绍程序设计语言发展过程。
Lecture 2
Syntax

3月1日前提交本次作业。

1*. 阅读John Backus的《Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs》，写一篇不少于2页的简单文献报告，对函数式程序设计语言和命令式程序设计语言进行比较。
Lecture 3
Operational Semantics

 

 
Lecture 4

Part 1: Operational Semantics (Continued) 

Part 2: Denotational and Axiom Semantics

3月12日前提交本次作业。

1. 本讲Part 1课件中的Exercise 1和2。 
Lecture 5
Lexical and Syntax Analysis
Lecture 6
Name, Bindings and Scopes
  
Lecture 7

Part 1: Name, Bindings and Scopes (Continued) 

Part 2: Data Types

3月24日前提交本次作业。

1.  本讲Part 1课件中的Exercise。
Lecture 8
Data Types (Continued)

3月31日之前提交本次作业。 

1. 对于简单的赋值语句A=B，哪些类型的A和B在C++中是合法的但在Java里头不是合法的？写出程序并附上运行结果截图。 

2. 对C的malloc和free函数跟C++的new和delete运算符进行分析比较，主要考虑安全性。 
Lecture 9

Part 1: Expressions and Assignment Statements

Part 2: Statement-level Control Structures

4月10日之前提交本次作业。

1. 解释为何在C语言中难以消除函数的副作用。

2. 用Java或C++写一个程序，在其中进行大量的浮点数运算以及相同数量的整数运算，比较两种运算所花费的时间。

3. 用Java或C++写一个程序，展示当表达式中的一个运算分量是函数调用时，运算分量求值顺序的规则。 
Lecture 10
Statement-level Control Structures (Continued)
  
Lecture 11
Subprograms
  
Lecture 12

Part 1: Subprograms (Continued)

Part 2: Implementing Subprograms

  
Lecture 13

Part 1: Implementing Subprograms (Continued)

Part 2: Abstract Data Types and Encapsulation Constructs

5月1日之前提交本次作业。

1. 写一个程序，使其在按引用传递和按值-结果传递方式传递参数时产生不同的结果，语言不限。

2. 对以分数形式给出的有理数设计并用C++、Java或Python语言实现一个抽象数据类型，至少包括构造函数及如下方法：获取分子，获取分母，有理数的加、减、乘、除运算，相等测试。 
Lecture 14

Part 1: Abstract Data Types and Encapsulation Constructs (Continued)

Part 2: Object-Orientation (I)

  
Lecture 15
Object-Orientation (II)
  
Lecture 16
Concurrency
  
Lecture 17
Exception Handling and Event Handling
  
Lecture 18
 前沿论文报告1（5月18日）

何家亮：Learning Formulas in Finite Variable Logics

倪新鹏：Elipmoc: advanced decompilation of Ethereum smart contracts 
Lecture 19
 前沿论文报告2（5月25日）

赵振华：Abstract interpretation repair

徐紫云：Choosing mathematical function implementations for speed and accuracy 
 Lecture 20 前沿论文报告3（5月29日）

陈欣：High-Throughput Garbage Collection

李翔宇：On type-cases, union elimination, and occurrence typing

 Lecture 21 前沿论文报告4（6月1日）

栾晓坤：Leapfrog: certified equivalence for protocol parsers

赵逸飞：Generating circuits with generators
 Lecture 22 前沿论文报告5（6月8日）

李夏鲲：One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes

张益豪：SolType: refinement types for arithmetic overflow in solidity