Programming Language Foundations in Agda and Arend

This is the PLFA book with all code snippets rewritten in Arend.

The book is a collection of markdown files, you can read it right here on GitHub. If you want to interact with the code snippets, clone the repo and open in IntelliJ IDEA with Arend plugin installed.

PLFA version: 22.08.

Arend version: 1.10.

Progress

Part 1: 10/10 sections completed.

Part 2: 1/11 sections completed.

Part 3: 0/5 sections completed.

Attribution

This project is based on the "Programming Language Foundations in Agda" by Philip Wadler, Wen Kokke and Jeremy G. Siek, licensed under CC-BY-4.0. I copy each page of the book and add Arend code snippets alongside the original Agda ones. I also include solutions to the exercises in Arend.