Course: | Type Systems and Programming Languages |
Properties: | Elective course E5: Software, 4 credits (6 ECTS) |
Semester: | Fall 2020 |
Instructor: | Polyvios Pratikakis |
Email: | polyvios@ics.forth.gr |
Where: | By zoom teleconference (password "lambda") |
Lecture 1 |
Introduction | TAPL, Chapters 1, 2. |
Lectures 2-3 |
Ocaml | Text: There are several online OCaml books and tutorials.
Reading: Patterson's Research Talk |
Lecture 4 |
Simple arithmetic: syntax, semantics, evaluation | TAPL, Chapters 3, 4.
Homework 1 out: Ocaml functions. Homework 1 due: 14 Oct., 23:59. |
Lecture 5 |
Untyped lambda calculus: syntax, basic examples | TAPL, Chapter 5.
Reading Assignment: Landin, P. J. (1966). The next 700 programming languages. Communications of the ACM, 9(3), 157-166. Due before class. |
Lecture 6 |
Untyped lambda calculus: semantics and implementation | TAPL, Chapters 6, 7. |
Lecture 7 |
Untyped lambda calculus: Writing the interpreter | Examples, guideline, exercises
Reading Assignment: P. Wadler, 2000. Proofs are Programs: 19th Century Logic and 21st Century Computing. (pdf) |
Lecture 8 |
Types and type rules | TAPL, Chapter 8. |
Lecture 9 |
Simply typed lambda calculus: The function type | TAPL, Chapter 9.
Reading Assignment: Edsger W. Dijkstra. Recursive programming. In Saul Rosen, editor, Programming Systems and Languages, chapter 3C, pages 221-227. McGraw-Hill, New York, 1960. AND Edsger W. Dijkstra. Go to statement considered harmful. 11(3):147-148, March 1968. Due before class. Homework 2 out: A lambda calculus interpreter Due: 29 Oct.. |
Lecture 10 |
Simply typed lambda calculus: Typechecking | TAPL, Chapter 10. |
Lecture 11 |
Adding more types: unit, tuples, pairs, sums, variants, lists, etc | TAPL, Chapter 11.
Homework 3 out: Write the typechecker for the function, bool, unit types Due: 13 Nov.. Reading Assignment: C. A. R. Hoare. Communicating Sequential Processes. 1978. |
Midterm |
in class | |
Lecture 12 |
Memory and References | TAPL, Chapter 13. |
Lecture 13 |
Subtyping | TAPL, Chapters 15, 17.
Reading Assignment: Luis Damas and Robin Milner. Principal Type-Schemes for Functional Programs. 1982. |
Lecture 14 |
Recursive types | TAPL, Chapter 20. |
Lecture 15 |
Curry-Howard isomorphism | |
Lectures 16, 17 |
The control-flow graph | PPA, Chapters 2, 3.
Reading Assignment: Necula, George C. "Proof-carrying code." Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1997. |
Lecture 18 |
Alias analysis: Unification | Reading Assignment: Points-to analysis in almost linear time |
Lecture 19 |
Alias analysis: Subtyping |
Reading Assignment:
Program Analysis and Specialization for the C Programming Language
Pointer analysis: haven't we solved this problem yet?, Michael Hind |
Lectures 20-21 |
Hoare Logic | LICS:MRAS, Chapter 4.
A. Hoare, An axiomatic basis for computer programming. |
Final |
Final exam | Final project report due |