Example: undefined behavior in a metafunction (March 2019)

Worked example of a reduction that gets stuck due to a metafunction under the Transient semantics of Big Types in Little Runtime (POPL 2017). Bottom line: it's tricky to pinpoint what subterm of a type is at fault when a type-tag check fails.

Survey response in `Languages in Racket: A Cultural Anthropology' (September 2018)

Jesse Alama wrote a thoughtful survey about language-oriented programming in Racket and collected responses from 30 "seasoned Racket developers" into a book. I am a respondent.

CS4500 git reference (September 2018)

Quick reference for the git command-line tool. Covers:

Sampling Gradual Typing Performance (May 2018)

This post explains the sampling method introduced in the paper On the Cost of Type-Tag Soundness. [src]

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 for a companion blog post. [src]

Type Tailoring (April 2017)

Type tailoring is a technique for adding domain-specific type checkers to a typed host language. Using the Type Systems as Macros approach to building typed languages, implementing type tailoring in Typed Racket is straightforward. Any library can apply the core idea, and you can try programming with type tailorings by downloading the trivial package (requires Racket v6.4 or later). [src]

Building a Website with Scribble (May 2017)

The source code for the PRL website is written using Scribble, the Racket documentation tool. I am very happy with this choice, and you should be too! [src]

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 quick discussion 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:

Languages as Dotfiles (March 2017)

Tired of writing (require (for-syntax syntax/parse)) at the top of your Racket programs? This post shows how to make a #lang to customize your default programming environment. [src]

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:

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.

A Few Cores too Many (August 2016)

Performance matters for software systems, but performance is not always easy to measure. At the PRL we recently had a scare with some unreliable measurements. Here is the story. [src]

Tutorial: Zero to Sixty in Racket (August 2016)

Racket is excellent for incrementally growing scripts into full-fledged programs. This post steps through the evolution of one small program and highlights the Racket tools that enable incremental advances. [src]

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.

Calendar Computations (January 2012)


Revision and extension of a calendar computations module from the Cornell Math Explorer's Club. This is probably the first .tex document I wrote that wasn't for a homework assignment.