(Oct 2) Exercise A is now available. Due in class on Thursday, October 8th.
(Sep 28) Nilesh Mahajan is the AI for the course. He will have office hours on Wednesdays 2-3pm.
(Sep 25) Homework 2 is available below. I have also added links to various OCaml resources that you will likely need for this assignment. For the written part, there is a LaTeX template available below. Please submit hw2 here.
(Sep 15) Submit homework here. (For hw1 you must submit a PDF file)
(Sep 14) There was a small but critical typo in Homework 1, question 5(b). It said: "Write an abstraction function... equivalent to lambda x.e"; that last part should read "... equivalent to lambda x.epsilon." Both the Homework 1 handout and solution template have been fixed.
(Sep 12) A template for Homework 1 is available below.
(Aug 30) Welcome to B522. There will be no class on Tues, Sept 1st; please read Pierce, chapters 1 and 2. The first class will meet on Thurs, Sept 3rd.
Classes meet on Tuesday and Thursday, 11:15am to 12:45pm in Lindley Hall 115. |
Amal Ahmed |
Office: Lindley 301G |
Phone: 855-4579 |
Email: amal at cs.indiana.edu |
Office hours: Monday 2-3pm, Thursday 2-3pm |
Nilesh Mahajan |
Email: nnmahaja at indiana.edu |
Office hours: Wednesday 2-3pm in Lindley 230A |
This course is aimed at Masters students, beginning PhD students, and high-level undergraduates in computer science with a keen interest in the theory and design of programming languages. The only requirement for the course is a considerable degree of mathematical maturity as obtained, for instance, through rigorous undergraduate coursework in discrete mathematics, algorithms and elementary logic. Familiarity with a higher-order functional programming language (e.g., Scheme, ML, Haskell, etc.) would be useful but is not required.
These books are excellent sources for the course, so purchasing them is a good idea. If you don't have a copy, IU library has an electronic version of Pierce that can be accessed by searching the IU catalog and providing your indiana.edu username and passphrase. Winskel will be on reserve at Swain Library.
Some other useful texts that provide a different perspective or more depth in some areas are:There will be an in-class midterm exam on Thursday, Oct 22nd.
There will be a 24-hour take-home final examination during the exam period at the end of the semester.
There will be 6 homework assignments during the course of the semester. Assignments will typically be made available on Thursdays and will be due back the following Thursday.
If a significant percentage of the class does poorly on one or more problems on the homework, the instructor may reassign those problems. Such assignments to redo a specific part of a homework will typically be announced on a Tuesday. You will have two days to submit a revised solution (due back by midnight on the due date). The score obtained on the revised solution will replace the earlier score received for that problem. This policy is aimed at ensuring that the emphasis is properly on learning the course material, and not on simply "getting through" the assignments. Note that due dates for homework revisions are marked with an "r" suffix on the schedule (e.g., hw1r).
All homeworks are due by 3pm on the due date unless otherwise specified. Extensions are granted only in extenuating circumstances at the discretion of the instructor. All written assignments must be typeset (using LaTeX) in the interest of legibility. Instructions for submitting a programming assignment will be given with the assignment.
You are responsible for reading the departmental statement on academic integrity before starting the first homework.
Unless explicitly instructed otherwise, all homework and exam work is to be solely your own, and may not be shared with or borrowed from any other person in the course. You are not permitted to draw upon assignments or solutions from similar instances of the course, nor to use course materials (such as assignments or programs) obtained from any web site or other external source in preparing your work.You are encouraged to discuss homework assignments with other students in the class, but you must adhere to the whiteboard policy. At the end of the discussion the whiteboard must be erased and you must not transcribe or take with you anything that has been written on the board (or elsewhere) during your discussion. You must be able to reproduce the results solely on your own after any such discussion.
The final grade will be comprised of homework (60%), midterm exam (15%) and final exam (25%) scores.
(Subject to change)
# | Date | Topics | Readings* | Lecture Notes | out | in | |
---|---|---|---|---|---|---|---|
Operational semantics and proof techniques |
|||||||
Sep | 1 | No class | P1,2 | ||||
1 | 3 | Introduction; Lambda calculus | P3 | syllabus, lecture1 | |||
2 | 8 | Structural Operational Semantics, CBV vs. CBN, recursion | P5 | lecture2 | |||
3 | 10 | Lambda calculus encodings, equivalence, reduction, normal forms | P5.2 | lecture3 | hw1 | ||
4 | 15 | OCaml tutorial (Roshan James) | |||||
5 | 17 | IMP introduction | W2 | lecture5 | hw1 | ||
6 | 22 | IMP small-step and big-step SOS | hw1r | ||||
7 | 24 | Inductive definitions, well-founded induction, rule induction | P3.2,3.3, W3,4 | lecture7 | hw2 code | hw1r | |
8 | 29 | Evaluation contexts, semantics by translation | lecture8 | ||||
Language features and translations |
|||||||
9 | Oct | 1 | uML and strong typing | lecture9 | exerciseA | hw2 | |
10 | 6 | uML; Run-time type checking | hw2r | ||||
11 | 8 | Naming and scope; Modules | lecture11 | hw3 | hw2r | ||
12 | 13 | State and mutable variables | lecture12 | ||||
13 | 15 | Translation from uML+references to uML | hw3 | ||||
14 | 20 | Continuation-passing style, CPS conversion | lecture14 | ||||
22 | Midterm (in class) | hw3r | |||||
Static semantics (type systems) |
|||||||
15 | 27 | Midterm discussion | |||||
16 | 29 | Simply-typed lambda-calculus | P8.1,8.2,9.1,9.2 | hw4 | hw3r | ||
17 | Nov | 3 | Type safety | P8.3,9.3-9.5 | |||
18 | 5 | Products, sums, recursion and more | P11 | hw5 | hw4 | ||
19 | 10 | References | P13 | hw4r | |||
20 | 12 | Exceptions | P14 | hw4r | |||
21 | 17 | Subtyping | P15.1-15.6 | hw5 | |||
22 | 19 | Recursive types | P20 | lecture22 | hw6 | ||
23 | 24 | Parametric polymorphism | P23 | ||||
26 | No class: thanksgiving break | ||||||
24 | Dec | 1 | Propositions as types | Wadler, P9.4 | lecture24 | hw5r | |
25 | 3 | Strong normalization and logical relations | P12 | lecture25 | hw6 | ||
26 | 8 | Existential types | P24 | hw6r | hw5r | ||
27 | 10 | Object-oriented features, object encodings | P18 | hw6r |
P = Pierce, W = Winskel