课程名称 (Course Name) ：程序语言理论 （Principles of Programming Language ）
课程代码 (Course Code）：X037515
学分/学时 (Credits/Credit Hours)： 3/48
开课时间 (Course Term )： fall
开课学院（School Providing the Course）: 软件学院(School of Software)
任课教师（Teacher）: 蔡小娟 (Xiaojuan Cai)
课程讨论时数（Course Discussion Hours）:
课程实验数（Lab Hours）: 0
课程内容简介(Course Introduction):
本课程的总体目标是让学生了解类型与程序语言的基本理论、方法和现有成果。我们将以函数式语言为载体，介绍计算机科学中的类型理论及其在程序语言中核心作用。主题包括无类型Lambda演算、简单类型系统、类型推导、带全称量词的类型、子类型、递归类型等。每一个主题都在实际程序语言中有所体现，其中子类型和递归类型部分，本课程还将详细介绍它的实现难点。
The purpose of this course is to introduce the basic principles, methods, and results of types and programming languages to graduate students. It provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each topic is motivated by programming examples and the more theoretical sections are driven by the needs of implementations.
The topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators.
教学大纲(Course Teaching Outline):
|
Topics
|
hours
|
|
Introduction and operational semantics
|
4
|
|
Introduction to Ocaml language
|
4
|
|
Untyped lambda calculus
|
4
|
|
Simple type system and simply typed lambda calculus
|
|
|
Type safety
|
4
|
|
Universal types and existential types
|
4
|
|
Type reconstruction
|
4
|
|
Subtyping and its meta theory
|
6
|
|
Recursive types and co-induction technique
|
6
|
|
Type operators and kinds
|
4
|
课程进度计划(Course Schedule):
|
Topics
|
|
|
Introduction
|
Lecture 1
|
|
Introduction to Ocaml language
|
Lecture 2
|
|
Untyped lambda calculus
|
Lecture 3
|
|
Simple types
|
Lecture 4
|
|
Type safety
|
Lecture 5
|
|
Universal types and existential types
|
Lecture 6
|
|
Type reconstruction
|
Lecture 7
|
|
Subtyping and its meta theory
|
Lecture 8
|
|
Recursive types and co-induction technique
|
Lecture9& Lecture 10
|
|
Type operators and kinds
|
Lecture 11
|
课程考核要求(Course Assessment Requirements)：
最后的分数由平时作业和期末笔试组成，期末考试为闭卷
final score = 30%homework + 70% final exam (close-book)
参考文献(Course References)：
Benjamin C. Pierce. Types and Programming Languages. The MIT Press. ISBN 0-262-16209-1.
预修课程（Prerequisite Course）
Principles of Compilers
