CS7480  Special Topics in PL:
Types, Contracts, Gradual Typing, and Compiler Correctness

Fall 2015

Blog

[Sep 18]   By Monday, Sept 21st, send me a ranked list with your top 3 choices of dates/papers you'd like to present (with subject "CS7480 Preferences").

Also, see: Reading, presenting, and writing critiques of papers.

---

[Sep 18]   Some students have asked about the amount of detail required when proving type safety on hw1. Specifically, for Problem 1, part (c), I expect you to:

• State (without proof) the inversion lemma, the canonical forms lemma, the permutation and weakening lemmas.
• State and prove the substitution lemma.
• Give detailed proofs of the progress and preservation lemmas. Make sure that you justify each step of the proof (e.g., application of some lemma or appeal to induction hypothesis), say what you are applying the induction hypothesis to and state exactly what you get by appealing to the induction hypothesis.

If you are unsure of stylistic issues when writing out proofs, refer to TAPL or come see me.

---

[Sep 12]   Here are links to the two SNAPL papers I mentioned in class on Thursday:

• The Racket Manifesto, Felleisen et al., SNAPL 2015


• Verified Compilers for a Multi-Language World, Ahmed, SNAPL 2015

---

[Sep 12]   If you haven't taken IPPL (CS 7400), make sure you do the Background Reading posted on the course webpage.

---

[Sep 9]   Welcome to CS7480!

Amal Ahmed

Last modified: Fri Sep 18 14:59:17 EDT 2015