Design Principles of Programming Languages / Spring 2025
Introduction
New programming languages have been emerging constantly. How do people propose the design of those languages? How do people formulate new high-level language features? Do various programming paradigms---such as object-oriented programming, functional programming, and generic programming---share a common theoretical foundation? This course will give an answer to those questions from the perspective of type theory.
Type theory is the core of many principles and methodologies that guide programming-language design. In modern programming languages, type annotations provide a basic means to avoid programming errors, and type theory provides characterizations of well-behaved type systems and methods for formulating complex types. This course will teach programming-language theory and organize around type theory.
Through this course, students can acquire a solid theoretical foundation and practical ability in the area of programming languages, as well as become capable of conducting programming-language-related research and designing new programming languages.
Course Information
Room: Changping 109
Time: Week 1–16, Monday, Lect. 7–9
Syllabus
Overview
In the past few decades, the development of programming languages has shown two distinct trends: (i) from simple low-level languages to complex high-level languages, and (ii) from a fixed small set of languages to many domain-specific languages. Traditional programming languages such as C and Java, which once dominated every programming language rankings, have been gradually surpassed by modern programming languages such as Python, JavaScript, Go, and Rust. On the one hand, many traditional languages have been evolving constantly and introducing various high-level language features. For example, the original design goal of Java was a simplified language, but the design of the latest Java has included many advanced features such as generics, functional programming, and dynamic features (e.g., reflection). On the other hand, more and more programming languages are constantly emerging to meet the needs of using specialized programming languages in specific application domains.
In this situation, the ability to design new programming languages is no longer an exclusive superior skill of senior programming-language researchers or frontier computer scientists; instead, it has become a necessary ability for software developers. Meanwhile, understanding and mastering the principles of programming-language design can also help us better understand various new features in high-level programming languages and make better use of mainstream programming languages.
In this course, we will address how the constantly emerging programming languages are designed, how new advanced language features are added to mainstream languages, and whether new programming paradigms such as object-oriented programming, functional programming, and generic programming have a common theoretical foundation.
To guide the design of programming languages, researchers have proposed a series of principles and methodologies, the most central one among which is type theory. Type annotations provide a basic means to avoid programming errors in modern programming languages, and type theory provides both characterizations of well-behaved type systems and methods for formulating complex types. This course will teach modern programming-language theory and organize around type theory.
This course has two characteristics: (i) rigor: all concepts in this course will have strict mathematical definitions that can be used by formal deduction and induction, rather than vague conceptual introductions, and (ii) practicality: all important concepts will be implemented through programming assignments and students can therefore master the knowledge through hands-on exercises. We hope that through this course, students will acquire a solid theoretical foundation and practical ability in the area of programming languages, as well as become capable of conducting programming-language-related research in academia and designing new programming languages in the industry.
Bibliography
Types and Programming Languages, Benjamin C.Pierce, The MIT Press, 2002. (Textbook)
Practical Foundations for Programming Languages, Robert Harper, Cambridge University Press, 2016. (Reference)
Implementation
The reference OCaml implementations of Types and Programming Languages can be found at the textbook’s official page.
This year, we plan to switch from OCaml to MoonBit. The port of some checkers used in the course can be found at https://github.com/pku-dppl/TAPL-in-MoonBit/.
Schedule
| Class | Date | Topic and Readings | Lecturer |
|---|---|---|---|
| 1 | 17-Feb | Introduction Untyped Arithmetic Operations |
Zhao |
| 2 | 24-Feb | OCaml/MoonBit | Zhao/Wang |
| 3 | 3-Mar | Lambda Calculus Nameless Representation |
Zhao |
| 4 | 10-Mar | Type Basics Simply Typed Lambda Calculus Simple Extensions |
Zhao |
| 5 | 17-Mar | Reference | Zhao |
| 6 | 24-Mar | Exception | Zhao |
| 7 | 31-Mar | Subtyping Metatheory of Subtyping |
Zhao |
| 8 | 7-Apr | Project Proposal (Midterm Test) |
Zhao/Wang |
| 9 | 14-Apr | Recursive Types | Wang |
| 10 | 21-Apr | Variable Types | Wang |
| 11 | 28-Apr | Type-Level Computation | Wang |
| 12 | 5-May | May Festival (No Class) | / |
| 13 | 12-May | Type Inference | Wang |
| 14 | 19-May | Substructural Types | Wang |
| 15 | 26-May | Effect Types | Wang |
| 16 | 2-Jun | Project Final Presentation | Zhao/Wang |
Previous years
- Spring 2022
- Spring 2023
- Spring 2024
- Spring 2025
Teaching assistants
Qihao Lian
mepy@stu.pku.edu.cn