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

时间：周二3-4节（双），周四5-6节。

地点：三教404。

答疑：单周二10:00-11:00，智华楼353。

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

教材及参考书目：

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

本课程期末成绩将基于平时成绩（课堂表现及作业20%）、前沿论文报告（30%）和课程研究论文（40%-50%）综合评定。

重要日期（deadline）：

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

    确定报告题目及课程论文所选课题（课程微信群接龙或发email至sunmeng@math.pku.edu.cn）：3月31日。

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

课程论文可选课题：

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

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

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

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

    5. Mediator的X语言代码生成：自选一种程序设计语言或形式规约语言（C++/Java/Python/UPPAAL/muCRL2/B/Event-B/...），实现从Mediator模型到该语言程序代码的生成工具。（独立或合作完成，合作者不超过2人，50%）

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

课程日程安排：

序号 课程内容 作业
Lecture 1
Introduction

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

1. 一种语言中特征过多会导致哪些问题？

2. 你支持还是反对在所有程序设计领域使用同一种语言，说明理由。

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

4. 编译和纯解释的方法实现语言各有什么优点？
Lecture 2
Syntax

Lecture 3
Operational Semantics

 

 
Lecture 4

Denotational and Axiom Semantics

3月14日之前提交本次作业：

课件中的Exercise 1和2。

Lecture 5
Lexical and Syntax Analysis
Lecture 6
Name, Bindings and Scopes
  
Lecture 7

Data Types (I)

Lecture 8
Data Types (II)

4月7日前提交本次作业：

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

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

Expressions and Assignment Statements

Lecture 10
Statement-level Control Structures
  
Lecture 11
Subprograms
  
Lecture 12

Implementing Subprograms

  
Lecture 13

Abstract Data Types and Encapsulation Constructs

Lecture 14

Object-Orientation

  
Lecture 15
Concurrency
  
Lecture 16
Exception Handling and Event Handling
  
Lecture 17
前沿论文报告1（5月15日）

魏泽明：Input-Relational Verification of Deep Neural Networks
Lecture 18
前沿论文报告2（5月20日）

陈品璋：A Core Calculus for Document: Or, Lambda: The Ultimate Document

丁天仪：SMT2Test: From SMT Formulas to Effective Test Cases
Lecture 19
前沿论文报告3（5月22日）

邵凯诚：Deciding Asynchronous Hyperproperties for Recursive Programs
Lecture 20 前沿论文报告4（5月29日）

伍思亦：Parametric Subtyping for Structural Parametric Polymorphism

王秭如：Automated Verification of Fundamental Algebraic Laws

Lecture 21 前沿论文报告5（6月3日）

岳关璋：Oxidizing OCaml with Modal Memory Management

黄安渝：Programming-by-Demonstration for Long-Horizon Robot Tasks 
Lecture 22 前沿论文报告6（6月5日）

林与心：PyDex: Repairing Bugs in Introductory Python Assignments using LLMs