Date

Lecture

Readings

Deliverable

1/28

No class

Illustrated Guide to a PhD, Might

1/30

Welcome; Syntax & semantics

I.1, I.2

PS1

2/4

Reduction in context

II.11

2/6

Redex

I.3

2/11

Types and abstract interpretation with types

I.4, II.12

2/13

Snow day

I.5

PS2

2/18

Abstract interpretation with intervals and type inference with constraints

I.10

2/20

The λ-calculus

2/25

The λv-calculus

Syntactic Approach to Type Soundness, Wright & Felleisen

2/27

Mixed mode secure computation (Aseem Rastogi); Incremental computation (Matthew Hammer)

A Simple Algorithm and Proof for Type Inference, Wand; Adapting Scrum to Managing a Research Group, Hicks & Foster

3/4

Type inference

Introduction to Set Constraint-Based Program Analysis, Aiken

RP2

3/6

Flow analysis & constraints

PS3

3/11

Symbolic execution

All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but might have been afraid to ask), Schwartz, Avgerinos, & Brumley; Directed Symbolic Execution, Ma, Khoo, Foster, & Hicks

3/13

Abstract interpretation

Abstract Interpretation: a Semantics-Based Tool for Program Analysis, Jones & Nielson; Systematic Design of Program Analysis Frameworks, Cousot & Cousot

3/18

Spring break

3/20

Spring break

3/25

State & control

A Formulae-as-Types Notion of Control, Griffin

3/27

Contracts

Contracts for Higher-Order Functions, Findler & Felleisen; On contract satisfaction in a higher-order world, Dimoulas & Felleisen

4/1

Polymorphism

RP3

4/3

Constraints for contracts

4/8

Abstracting abstract machines

Abstracting Abstract Machines, Van Horn & Might

4/10

Symbolic execution for contracts

Higher-Order Symbolic Execution via Contracts, Tobin-Hochstadt & Van Horn

4/15

Computational complexity

Linear lambda calculus and PTIME-completeness, Mairson; Deciding kCFA is complete for EXPTIME, Van Horn & Mairson

4/17

Type checking & inference via reduction

III.23

4/22

Dependent types

Kris Micinski lecture

4/24

System F

4/29

Slack

5/1

Presentations: Projects 3, 7, 2

RP4

5/6

Presentations: Projects 10, 9, 4

5/8

Presentations: Projects 8, 5, 6

5/13

Presentations: Project 1

5/21

Final exam

PS4 and RP5