ImplementingSomeFunctionsAndTheoremsInTheBookTypesAndProgrammingLanguagesByBenjaminPierce

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

• The report
• The Agda code

The code is tested and works with Agda version 2.2.2.