Date

Lecture

Readings

Deliverable

9/1

No class

Illustrated Guide to a PhD, Might

9/3

No class

Preface, I.1, I.2

PS1

9/8

Welcome; Syntax & semantics

II.11

9/10

Modelling semantics in OCaml

I.3

9/15

Modelling semantics in Redex

I.4, II.12

9/17

Reduction with evaluation contexts

I.5

9/22

Meaningful Errors

I.10

9/24

Type checking; type-based abstract interpretation

Syntactic Approach to Type Soundness, Wright & Felleisen

9/29

Interval abstraction

A Simple Algorithm and Proof for Type Inference, Wand

PS2

10/1

Functions; type inference; unification

Symbolic Execution and Program Testing, King

10/6

Project pitches: Hammer, Mardziel, Micinski

Definitional Interpreters for Higher-Order Programming Languages, Reynolds

PS3

10/8

Defunctionalization & CPS

Introduction to Set Constraint-Based Program Analysis, Aiken

10/13

Abstract machines

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

RP1

10/15

Flow analysis & constraints

Abstract Interpretation: a Semantics-Based Tool for Program Analysis, Jones & Nielson

10/20

Dependent types

Systematic Design of Program Analysis Frameworks, Cousot & Cousot

10/22

Project collaboration

A Formulae-as-Types Notion of Control, Griffin

RP2

10/27

Modelling imperative state

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

10/29

Abstracting abstract machines (I); Church encodings

Abstracting Abstract Machines, Van Horn & Might

11/3

Abstracting abstract machines (II)

11/5

Computational complexity

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

11/10

Symbolic Execution

11/12

Symbolic execution for contracts

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

11/17

Type checking & inference via reduction

III.23

PS4

11/19

Dependent types

11/24

System F

11/26

No class: Thanksgiving

12/1

Slack

12/3

Slack

RP3

12/8

Presentations: Project 19, 21, 23, 25

12/10

Presentations: Project 22, 24, Li, Darais

12/19

Final

RP4, PS5