# 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.