(Jan 7) Welcome to CS7470!
| Mondays and Wednesdays 2:50-4:30pm in Hayden Hall 321 |
| Amal Ahmed |
| Office: WVH 328 |
| Email: amal at ccs.neu.edu |
| Office hours: by appointment (email me) |
Students should propose three “influential ideas” of interest, ordered from most preferred to least preferred, each supported by at least one central citation. (See suggested papers for potential starting points.)
Due date: Send the list by January 12. Have a 15-minute meeting with the instructor on January 14 or 15 to discuss the topic. Topics will be approved by January 16.
Once a topic is approved, compile a list of three to six major publications that capture the evolution of the idea. Read the introductory part of each article so that you can explain its role in the evolution of the influential idea.
By January 20, submit a list of references to the instructor. Each reference should consist of the author(s), the title, a PDF link, and a sentence or two explaining your understanding of the role of the paper.
Set up a meeting with the instructor to discuss the proposed sequence of articles. This meeting will decide which articles to use.
Write a short abstract that explains the basics of the influential idea and its evolution, as represented by the chosen papers.
Due date: Send the lecture title and abstract to the instructor as soon as possible after the selection meeting and before the presentation to the class.
Study the selected papers. Prepare an annotated bibliography of the chosen articles. Prepare a blackboard/whiteboard presentation.
Due date: Please have a draft of your presentation ready one week before your presentation. Then meet with the instructor if there are any questions about how to present the material, so changes can be made in a timely fashion.
If you are not presenting, you will assess the lecture given by the student presenting and submit your Assessment to the instructor. The assessments provide feedback on both the lecture content and presentation.
The schedule for the first round of lectures will be set up by roughly January 23rd. Everyone will present once before we repeat the above steps for the second presentation.
| Date | Topic | Presenter |
|---|---|---|
| W 1/7 | Type Abstraction
References:
|
Amal |
| M 1/12 | No class – POPL | |
| W 1/14 | No class – POPL | |
| M 1/19 | No class – Martin Luther King Jr. Day | |
| W 1/21 | Logical Relations and Parametricity
|
Amal |
| M 1/26 | Snow day -- 1-1 meetings to discuss presentations | |
| W 1/28 | Existential Types and Representation
Independence
References:
|
Amal |
| M 2/2 | Separation Logic
Separation logic developed out of a need for a more native way to reason about shared memory. It establishes an assertion language with two new operators — ∗ and —∗ ; (separating conjunction and "wand" respectively) — that allow clean description of heap states. The "vanilla" separation logic, discovered by a combination of Ishtiaq, O'Hearn, and Reynolds around 1999-2002, sparked a wave of new separation logics with features that allowed for new types of reasoning. This lecture will go over the fundamentals of separation logic and motivate the works that came after, culminating in a discussion of the context in which Iris came to be. Primary references:
|
Elan Semenova |
| W 2/4 | Did Linear Types Change the World? Types allow for tracking of what operations are possible on values: files can be opened and closed, locks can be acquired and released, memory can be allocated and deallocated. Although at any given moment, the real resource is only at one of these states, simply typed lambda calculus is not representative of this reality: it allows for resources to exist in multiple states at any given moment. Linear types allow us to address this and reject buggy programs as well as maintain language purity in certain scenarios. I will be talking about *why* these problems exist and *how* linear types address them, as well as the biggest application of linear types by far in the management of heap memory. Primary references:
|
Nikolay Tokarenko |
| M 2/9 | Refinement Types Type systems allow programmers to express and statically check specifications of program behavior. However, some programs have behavior that can only be expressed for some subset of a given type: for instance, some list functions may require a nonempty input or ensure that the length of their output remains unchanged; certain algorithms on propositional formulae require their input to be in a particular normal form. In many languages, these kinds of behavioral constraints are too granular to be expressed at the type level and so must be left implicit. Type refinement systems, however, enrich such type systems with a means to express properties requiring sub-type precision that the language's base type system cannot capture, allowing programmers to identify subsets of types satisfying properties of interest. This talk will present a simple calculus that introduces several core features of refinement types. It will then examine a particular style of type refinement known as datasort refinement, introduced by Freeman and Pfenning in 1991, which refines ML-like type systems with sorts defined over the inductive structure of data types. Finally, it will discuss several alternative approaches to type refinement that provide more expressive refinements using type-level term languages and more complex constraint-solving infrastructure. References:
|
Joseph Rotella |
| W 2/11 | No class | |
| M 2/16 | No class – Presidents’ Day | |
| W 2/18 | Modal, Linear, and Adjoint Logic (Part I, 50 mins) Abstract |
Cynthia Li |
| F 2/20 | Modal, Linear, and Adjoint Logic (Part 2, 50 mins) Abstract |
Cynthia Li |
| M 2/23 | Information Flow Abstract |
Bex Golovanov |
| W 2/25 | Higher-order Control-flow Analysis Abstract |
Vadym Matviichuk |
| M 3/2 | No class – Spring Break | |
| W 3/4 | No class – Spring Break | |
| M 3/9 | Title Abstract |
|
| W 3/11 | Title Abstract |
|
| M 3/16 | Proof-Carrying Code Abstract |
Owen Duckham |
| W 3/18 | Multi-Language Computation Abstract |
Luis Garcia |
| M 3/23 | Testing and Symbolic Execution Abstract |
Patrick Zheng |
| W 3/25 | Title Abstract |
|
| M 3/30 | Title Abstract |
|
| W 4/1 | Title Abstract |
|
| M 4/6 | Title Abstract |
|
| W 4/8 | Title Abstract |
|
| M 4/13 | Title Abstract |
|
| W 4/15 | Title Abstract |
|
| M 4/20 | No class – Patriots’ Day |