課程內(nèi)容：

本課程旨在讓學(xué)生能夠參與有關(guān)高級編程語言特性的技術(shù)討論，其中包括支撐當(dāng)代發(fā)展的核心概念。課程說明了關(guān)于程序含義的問題應(yīng)在嚴格的數(shù)學(xué)基礎(chǔ)上提出和解決，并介紹了在這一領(lǐng)域已經(jīng)取得的成就。對于那些希望深入了解編程語言的學(xué)生來說，這門課程能為你在該領(lǐng)域工作或繼續(xù)深造打下堅實的基礎(chǔ)。

教學(xué)大綱：

- 非類型lambda微積分

- 簡單類型的lambda微積分

- 證明方法：邏輯關(guān)系

- 程序的觀察等價性

- 簡單類型lambda微積分的函數(shù)模型

- PCF：現(xiàn)代函數(shù)式語言的核心

- PCF的指稱語義

- 高級主題（可能是多態(tài)性或并發(fā)性）研究

學(xué)習(xí)成果：

成功完成本課程后，學(xué)生將能夠：

1、描述和分析所學(xué)的各種計算模型中術(shù)語的行為。

2、計算程序和類型的指稱。

3、使用結(jié)構(gòu)歸納法證明程序的選定結(jié)果。

4、應(yīng)用編程語言的基本理論結(jié)果和特定技術(shù)來推理程序。

5、利用適當(dāng)?shù)募夹g(shù)和模型，用合適的編程語言證明程序的等價性。