(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) Modal logic is used for reasoning about knowledge and possibility. I present modal logic with possible worlds semantics and an axiomatic presentation. Then, I show Pfenning/Davies’s judgmental presentation of modal logic and how a Curry-Howard interpretation of that logic can be used to create a language for staged computation. In the second part of my presentation I discuss specifically the judgmental approach that Pfenning and Davies are using in “Judgmental Reconstruction”—what design choices are they making when creating logics, and what are the philosophical and practical reasons behind them? How might these choices translate to other logics? I highlight how using this judgmental approach with linear logic can reveal adjoint logic as a generalization over modal and substructural logics. References:
|
Cynthia Li |
| F 2/20 | Modal, Linear, and Adjoint Logic (Part 2, 50
mins, 12:00-12:50, 366 WVH) Continued from 2/18 |
Cynthia Li |
| M 2/23 | Blizzard day -- class online: Discussion of what makes a good lecture | |
| W 2/25 | Information Flow Reasoning about information flow frequently requires security labelling (ex. secret or public) for types/data. In 1998, Heintze and Ricke published the SLam Calculus, a language in the style of SML, which annotated types with security properties. In 1999, Abadi et al. utilized a monadic approach (DCC) to establish a calculus for reasoning about general program dependencies, including information flow. This lecture will begin with a brief overview of SLam and DCC, followed by a logical relations proof of noninterference for DCC and a discussion of recent results for weakening non-interference (declassification). Primary references:
|
Bex Golovanov |
| M 3/2 | No class – Spring Break | |
| W 3/4 | No class – Spring Break | |
| M 3/9 | Auto-Active Program Verification
A large part of the verification community uses tools like Dafny, F*, and Liquid Haskell which use SMT solvers such as Z3 to partially automate proofs. These tools are dubbed _auto-active_, since they combine the strengths of both automated theorem provers and interactive proof assistants. In this lecture, we will introduce the SMT solving ecosystem and show how these tools leverage SMT to build higher-level program logics. References:
|
Josh Gancher |
| W 3/11 | Higher-order Control-flow Analysis A lot of interesting compiler optimizations require information from a control-flow analysis. This is a straightforward process in a first-order language where control operators are part of syntax and therefore, it is easy to construct a control-flow graph. The story is more complicated in a higher-order language: lambda is a piece of data that has control and environment effects. So, in order to do control-flow, you need to do data-flow, and to do data-flow, you need to do control-flow. This lecture will talk about a popular framework to solve this problem (k-CFA) as well as work that followed after this research (ΓCFA, AAM) and applications of the CFA framework. References:
|
Vadym Matviichuk |
| M 3/16 | Proof-Carrying Code
Proof-carrying code (PCC) provides a way to safely execute untrusted native code without runtime overhead: the code producer supplies a formal safety proof alongside the code, and the consumer only needs to validate it—a one-time, simple, and fast operation. We begin with Necula and Lee's original PCC framework for safe kernel extensions, then examine foundational PCC (FPCC), which moves instruction semantics into the logic itself and correspondingly reduces what must be trusted. Sufficiently rich type systems can express many of the safety properties that PCC captures, embedding the safety argument in the typing derivation itself; type-preserving compilation leverages this by maintaining well-typedness through each compiler pass down to the target language, eliminating the need for a separate proof artifact. We trace this line of work and ask why it has not fully materialized thirty years later. Primary references:
|
Owen Duckham |
| W 3/18 | Multi-Language Computation via Language Boundaries
Multi-language computation exists all around us. Large systems are often made up of code in different languages. System designers and programmers need to think hard about how these pieces of code interact, especially in the presence of vastly different data representations and semantics. How do we reason about our code in this setting? With this question in mind, Matthews and Findler introduced a framework for reasoning about type soundness in a multi-language setting, centering on the use of language boundaries. This lecture explains what language boundaries are and how they have been used in research. Bibliography
|
Luis Garcia |
| M 3/23 | Testing and Symbolic Execution
Symbolic execution is the bridge between theorem proving and traditional testing methods, as it combines the power of constraint solving with the practicality of normal testing. The original symbolic execution work of James C. King laid the foundation for symbolic execution. It also suffered from a lot of limitations at that time. A DP algorithm walkthrough is presented on an example from symbolic execution to show how exactly one can solve SAT problem. DP, DPLL, and subsequent SAT/SMT techniques enabled tools that rely on constraint solving. EXE, with its powerful co-designed STP solver, improved and innovated upon the original vision of King. KLEE built upon EXE to address several of its limitations and presented us with a new way to do symbolic execution. Finally, I will conclude with some remarks on what makes a program analysis tool good based on the development of KLEE and reports from Google and Facebook. Primary References:
|
Patrick Zheng |
| W 3/25 | A Zoo of Logics
Hoare logic has some things it fundamentally can't express. In this talk, we discuss what the limitations of the Hoare triple definition are and use that to motivate Incorrectness Logic. After studying the definition and getting an intuition for what the triples say, we move on to motivating the development of predicate transformers and study the eight transformers Versht et.al. defines. Primary references:
|
Elan Semenova |
| M 3/30 | Foundations of Dependently Typed Proof Assistants A long line of philosophical work, dating back centuries, has sought to formalize and verify deductive reasoning by mechanical means. Through the Curry–Howard correspondence, dependent type theories can be fruitfully used as the basis of such computational systems, and have seen widespread use in modern proof assistants like Agda, Lean, and Rocq. This talk will discuss the theories that underlie these three systems, beginning with Martin-Löf’s intensional type theory and developing thereupon the Calculus of (Inductive) Constructions and its extensions. In so doing, it will also consider the relative metatheoretic trade-offs made by different CIC-based proof assistants. References:
|
Joseph Rotella |
| W 4/1 | Title Abstract |
Bex Golovanov |
| M 4/6 | Soft contract verification for higher-order programs Abstract |
Vadym Matviichuk |
| W 4/8 | Title (Part 1, 50 mins) Abstract |
Cynthia Li |
| Th 4/9 | Title (Part 2, 50 mins, 10:30-11:20, 366 WVH) Continued from 4/8 |
Cynthia Li |
| M 4/13 | Title Abstract |
Nikolay Tokarenko |
| W 4/15 | Title Abstract |
Owen Duckham |
| M 4/20 | No class – Patriots’ Day |