Type-and-scope safe programs and their proofs.

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Browse the full CPP paper archive.