Design Principles of Programming Languages / Spring 2023
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
Place：Changping 201
Time：Monday(7-9) From week 1 to week 16
Syllabus
Content
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 JavaScript, Erlang, and R. 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 8 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.(Book)
Course Arrangement
| Class | Date | Topic and Readings | Lecturer |
|---|---|---|---|
| 1 | 20-Feb | Introduction Untyped arithmetic operations |
Zhao |
| 2 | 27-Feb | OCaml | Zhao |
| 3 | 6-Mar | Lambda Calculus Nameless Representation |
Zhao |
| 4 | 13-Mar | Type Basics Simple Typed lambda Calculus Simply Extensions |
Zhao |
| 5 | 20-Mar | Reference | Zhao |
| 6 | 27-Mar | Class Project | Zhao |
| 7 | 3-Apr | Exception | Zhao |
| 8 | 10-Apr | Subtyping Metatheory Subtyping |
Zhao |
| 9 | 17-Apr | Middle Test (+ Check project) | Zhao/Wang |
| 10 | 24-Apr | Case Study: Imperative Objects Case Study: Featherweight Java |
Wang |
| 11 | 1-May | May Festival (No class) | / |
| 12 | 8-May | In-class Practice | Wang |
| 13 | 15-May | Recursive Types Metatheory of Recursive Types |
Wang |
| 14 | 22-May | Type Reconstruction Universal Types |
Wang |
| 15 | 29-May | Existential Types | Wang |
| 16 | 5-Jun | Final Presentation | Zhao/Wang |
Previous years
- Spring 2022
- Spring 2023
- Spring 2024
Teaching assistants
Lijuan Tang
lijuan_tang@stu.pku.edu.cn