Implementing Some Functions And Theorems In The Book Types And Programming Languages By Benjamin Pierce

This page contains the report and some code from a CSALL project:

The code is tested and works with Agda version 2.2.2.