X037515 Principles of Programming Language 程序语言理论

 

课程名称 (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

 

[ 2016-09-21 ]