Spring 2009
The course syllabus can be found here.
Lectures
Lecture
1. Introduction and Course Overview.
Lecture
2. A Language for Arithmetic Expressions.
Lecture
3. Introduction to Coq.
Lecture
4. Introduction to Operational Semantics.
Lecture
5. Natural and Contextual Semantics.
Lecture
6. Axiomatic Semantics.
Lecture
7. Introduction to Lambda Calculus.
Lecture
8. Lambda Calculus (cont).
Lecture
9. Introduction to Type Systems.
Lecture
10. Simply-Typed Lambda-Calculus.
Lecture
11. Simply-Typed Lambda-Calculus Extensions.
Lecture
12. Typing References and Exceptions.
Lecture
13. Introduction to Subtyping.
Lecture
14. Object-Oriented Programming.
Lecture
15. Self-Reference.
Lecture
16. Algorithmic Subtyping.
Lecture
17. Recursive Types.
Lecture
18. Introduction to System F.
Lecture
19. Existential Types.
Miscellaneous
A style guide for SML can be found
here.
An overview of Mini-ML can be found
here.
Announcements
Any questions and discussions related to the class can be posted on the
class blog
Midterm Exam: : March 11, 2009, 8PM - 9:30PM, BRNG 1254
Solutions to the Midterm can be
found here
Final Exam: May 4, 2009, 8AM - 10AM, LWSN 1106, closed-book, closed-notes.
Review slides
Exercises
1. (Lecture 4) Use Ott to typeset and generate Coq definitions for the
language of Boolean terms. Due Date: 2/4/09.
2. (Lecture 8) TAPL 5.3.7 and 5.3.8. Use Ott to typeset your solutions.
TAPL 6.2.5 and 6.3.1. Due Date: 2/23/09.
3. (Lectures 9 - 13) TAPL 11.12.2, 12.1.1, 13.1.12,13.4.1,14.1.1
4. (Lectures 13 - 15) TAPL 15.2.3, 15.2.4, 16.2.3, 16.2.6 Due Date: 4/10/09
5. (Lecture 17) TAPL 20.1.2, 20.1.4, 20.1.5. (For each of these questions,
present your solutions using an iso-recursive formulation.) Due Date:
4/24/09
5. (Lecture 18) TAPL 23.4.1, 23.4.6, 23.4.8, 23.4.12. Due Date:
5/1/09
Projects
1. An
interpreter using evaluation contexts. Due Date: February 20, 2009.
Turnin Instructions. turnin -c cs565 -p assignment1
2. A
normal-order interpreter for Mini-ML. Due Date: March 13, 2009.
3.
Subtyping for Mini-ML. Due Date: April 15, 2009.