Course: | Introduction to Type Systems and Static Analysis |
Properties: | Elective course E5: Software, 4 credits (6 ECTS) |
Semester: | Fall 2015 |
Instructor: | Polyvios Pratikakis |
Email: | polyvios@ics.forth.gr |
Lecture 123 Sept. |
Introduction | TAPL, Chapters 1, 2. |
Lectures 2-328, 30 Sept. |
Ocaml | Text: There are several online OCaml books and tutorials. |
Lecture 45, 7, 12 Oct. |
Simple arithmetic: syntax, semantics, evaluation | TAPL, Chapters 3, 4.
Homework 1 out: Ocaml functions. Homework 1 due: 18 Oct., 23:59. |
Lecture 514, 19 Oct. |
Untyped lambda calculus: syntax, basic examples | TAPL, Chapter 5. |
Lecture 621, 26 Oct. |
Untyped lambda calculus: semantics and implementation | TAPL, Chapters 6, 7. |
Lecture 702 Nov. |
Untyped lambda calculus: Writing the interpreter | Examples, guideline, exercises
Homework 2 out: A lambda calculus interpreter |
Lecture 804 Nov. |
Types and type rules | TAPL, Chapter 8. |
Lecture 909 Nov. |
Simply typed lambda calculus: The function type | TAPL, Chapter 9.
Homework 2 due: 16 Nov., 23:59. |
Lecture 1016 Nov. |
Simply typed lambda calculus: Typechecking | TAPL, Chapter 10.
Homework 3 out: Write the typechecker for the function, bool, unit types Homework 3 due: 08 Dec., 23:59. |
Lecture 1118 Nov. |
Adding more types: unit, tuples, pairs, sums, variants, lists, etc | TAPL, Chapter 11. |
Lecture 1220 Nov. |
Memory and References | TAPL, Chapter 13. |
Lecture 1323 Nov. |
Subtyping | TAPL, Chapters 15, 17. |
Lecture 1425 Nov. |
Recursive types | TAPL, Chapter 20. |
Lecture 1530 Nov. |
Curry-Howard isomorphism | |
Midterm02 Dec. |
Midterm exam | |
Lecture 16, 1707 Dec. |
The control-flow graph | PPA, Chapters 2, 3. |
Lecture 1809 Dec. |
Alias analysis: Unification | Points-to analysis in almost linear time |
Lecture 1914 Dec. |
Alias analysis: Subtyping |
Program Analysis and Specialization for the C Programming Language
Pointer analysis: haven't we solved this problem yet?, Michael Hind |
Lectures 20-2116 Dec. |
Hoare Logic | LICS:MRAS, Chapter 4.
A. Hoare, An axiomatic basis for computer programming. Project due |
Final?? Jan. |
Final exam | Final project report due |