Theory of Programming Language

Instructor	Phone	Email	Course Time	Place
Yu Zhang	3603804	yuzhang at ustc.edu.cn	Thursday 9:45~12:10	3214

C.A.R. Hoare. Hints on programming language design. Stanford University. Technical Report: CS-TR-73-403. 1973.
Niklaus Wirth(Pascal之父). On the Design of Programming Languages. Information Processing. 74, pages 386-393, New York, N.Y., 1974. North-Holland Publishing Co.
Peter Wegner. Programming languages - the first 25 years. IEEE Transactions on Computers, Vol. C-25, No. 12, pp. 1207-1225, 1976.
Guy L. Steele. Growing a Language. OOPSLA 1998 Keynote.
C.A.R. Hoare. An axiomatic basis for computer programming. CACM 12(10), 1969, pages 576 - 580.
Leslie Lamport. The Future of Computing: Logic or Biology.
Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing. June 2000, updated November 2000.
......

Coq Home page
- The Coq Proof Assistant – A Tutorial v8.1
- The Coq Proof Assistant – Reference Manual v8.1
Coq Art Home page (download)
Coq Tutorial in POPL08
Proof General (download)
How to install ...?
Coq practice: a simple language - Lnumstr

Date	Topics	Homework
Sep.10 Sep.17	1 Introduction(1in1, 6in1) [TPL]ch1;[TAPL]ch1~3;	Sep.10:[TPL]1.3 Sep.17:[TPL]1.5,1.6
Sep.17 Sep.24 Oct.10 Oct.15 Oct.22	2 The language PCF - Algebraic Datatype(1in1, 6in1) [FPL]ch2, ch3	Sep.24:[TPL]2.3 Oct.10:[TPL]2.4,2.10,2.13,2.16 Oct.15:[TPL]2.19,2.22,2.23 Oct.22:[TPL]2.30,2.33
Oct.29 Nov.5 Nov.12	3 Simply-typed Lambda Calculus(1in1, 6in1) [FPL]ch2, ch4	Oct.29:[TPL]3.6(c),3.8(b) Answer 2: 1,2,3,4, 5,6 Nov.5:[TPL]3.27(a)(b)(c), 3.28(a) Nov.12:补充题1in1, 6in1
Nov.12 Nov.19	4 Recursive Functions and Recursive Types(1in1, 6in1)	Nov.12:[TPL]4.2
Nov.19	Coq & its Application(1in1, 6in1) Install Coq Declarations and Definitions: bnat_1.v(bnat_1sol.v), Proposition logical verification: prop.v(propsol.v) Tactics: intro(s), split, left, right, exact, apply Symbols and strings: sym_str1.v, util.v	Nov.19:Coq Practice
Nov.26 Dec.3 Dec.10	5 Imperative Programs and Their Semantics(1in1, 6in1) Exceptions and Continuations(1in1, 6in1 7.2&7.3) [PFPL]ch29-31;[TPL]ch5 Resources of Continuations	Nov.26:[TPL]5.3
Dec.17	6 Propositions and Types(1in1, 6in1) [PFPL]ch32,33;[TPL]ch9
Dec.17 Dec.24	7 Polymorphism(1in1, 6in1) [PFPL]ch25,26;[TPL]ch7 Notice: Everyone must submit his reading report on or before Jan. 20.	Answer 3: 1,2,3,4, 5,6
Dec.31	Subtyping(Subtyping1in1) [PFPL]32;[TPL]ch10 Dynamic Typing(1in1, 6in1) [PFPL]22,23;[TPL]ch11