Date

Lecture

Readings

Deliverable

9/2

No class

Illustrated Guide to a PhD, Might

9/4

No class

Preface, I.1, I.2

PS1

9/9

Welcome; Syntax & semantics

II.11

9/11

Modelling semantics in OCaml & Redex

I.3

9/16

Reduction with evaluation contexts

I.4, II.12

9/18

Compositional compilation

I.5

9/23

Meaningful Errors

I.10

PS2

9/25

Type checking; type-based abstract interpretation

Syntactic Approach to Type Soundness, Wright & Felleisen

9/30

Type inference; unification

A Simple Algorithm and Proof for Type Inference, Wand

10/2

Interval abstraction; functions

Symbolic Execution and Program Testing, King

10/7

Project pitches: Hammer, Mardziel, Micinski

Definitional Interpreters for Higher-Order Programming Languages, Reynolds

PS3

10/9

Defunctionalization & CPS

Introduction to Set Constraint-Based Program Analysis, Aiken

10/14

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/16

Flow analysis & constraints

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

10/21

Dependent types

Systematic Design of Program Analysis Frameworks, Cousot & Cousot

10/23

Project collaboration

A Formulae-as-Types Notion of Control, Griffin

RP2

10/28

Modelling imperative state

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

10/30

Abstracting abstract machines (I); Church encodings

Abstracting Abstract Machines, Van Horn & Might

11/4

Abstracting abstract machines (II)

11/6

Computational complexity

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

11/11

Symbolic Execution

11/13

Symbolic execution for contracts

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

11/18

Type checking & inference via reduction

III.23

PS4

11/20

Dependent types

11/25

System F

11/27

No class: Thanksgiving

12/2

Slack

12/4

Slack

RP3

12/9

Presentations: Project 15, 14

12/11

Presentations: Project 18, 13, 16

12/20

Final

RP4, PS5