Implement your POPL paper

Implement your POPL paper (in Haskell)

A four-lecture tutorial on well-scoped de Bruijn indices for implementing type systems, interpreters, and program transformations.

Start with Lecture 1 Get the code on GitHub
Lecture 1

Well-Scoped De Bruijn Representations

Build the infrastructure from scratch: finite sets, binders, substitution environments, and a big-step evaluator for a simply-typed lambda calculus.
Lecture 2

Pattern binding (plus scope checking)

Use the rebound library to implement a language with (deep) pattern matching.
Lecture 3

Property-based testing

Generate well-scoped and well-typed lambda terms to enable property-based testing.
Lecture 4

CPS: A Scope-Preserving Translation

Implement continuation-passing-style conversion as a typed, scope-preserving term-to-term transformation, and test its correctness properties with QuickCheck.

About the tutorial

This series of four 50-minute lectures covers how to represent and manipulate lambda-calculus terms using well-scoped de Bruijn indices in Haskell. The goal is to provide a practical basis for implementation, suitable for experimenting with language and logic design.

The target audience is students and researchers familiar with lambda calculi and functional programming (Haskell, OCaml, Rocq, or Agda). Some prior exposure to dependently-typed programming is helpful.

Getting the code

The tutorial code is a self-contained Haskell project that depends on the rebound library on Hackage. 

git clone https://github.com/sweirich/rebound
cd rebound/tutorial/main
cabal build
cabal repl

You need GHC and Cabal, which you can install via GHCup.