Miscellaneous Lecture Notes

Racketeering 101 (October 2017)

Slides from a RacketCon 2017 tutorial on submitting a pull request to a package in the Racket main distribution. They slides aren't much to look at without the words to go with them.

See http://blog.racket-lang.org/ for a companion blog post.

Soft Typing (April 2017)

Notes from a HOPL 2017 lecture on the theme of Soft Typing. The actual talk covered the why, whence, what, with a few minutes discussion of the utiliy of Andrew Wright's soft type checker at the end.

These and other notes from HOPL 2017 are in the shared repo for the course: https://github.com/nuprl/hopl-s2017

Datalog for Static Analysis (February 2017)

Notes from a HOPL 2017 lecture on the theme of Datalog for program analysis.

These and other notes from HOPL 2017 are in the shared repo for the course: https://github.com/nuprl/hopl-s2017

ESP: Path-Sensitive Verification (October 2016)

Summary of ESP: Path-Sensitive Program Verification in Polynomial Time. The slides focus on the 5-stage process of running ESP on a program (rather than property analysis or the property simulation algorithm). Sorry the slides are rushed. Presented in Frank Tip's CS7480.

The IFDS framework (October 2016)

An overview of the IFDS framework for modeling and solving problems in static analysis, following the POPL 1994 paper. Presented in Frank Tip's CS7480.

Craig Interpolation (February 2016)

The very basics of Craig Interpolation, presented in Thomas Wahl's CS7485.

Summary: Kildall's Algorithm (January 2016)

Quick summary of Kildall's Algorithm for global static analysis. May be my favorite fixpoint. Presented at PL junior.

Summary: CBN, CBV, and the λ Calculus (December 2015)

Brief summary of the seminal work by Plotkin. Bottom line: languages and calculi must be developed together. Also it is possible to build (inefficient) order-of-evaluation-independent interpreters; however, a call-by-value language is marginally better for the task. Presented at PL junior.

CompCert Tutorial (November 2015)

A fast walk through the CompCert compiler. Goes over the architecture, correctness strategy, and correctness proof. Presented in CS 7480.

Coinduction Tutorial (March 2015)

Notes and code and references introducting coinduction, mostly through streams. Presented at Northeastern's PL junior seminar.

Logical Relations Tutorial (October 2014)

A brief overview of logical relations. Presented at Northeastern's PL junior seminar.