Lambda calc on CEK machine with call/cc

This is my term project for CSCI 8980: Programming Language Foundations in Agda during the Fall 2021 semester. It follows a textbook of the same name.

Assignment:

Your Agda project should be formalizing some language feature not detailed in the textbook and proving type safety of it. Your formalization should contain these three ingredients:

1. The statics: the type system.
2. The dynamics: a dynamic system that is different from the reduction system used in Part 2 of the textbook.
3. The theorems: progress and preservation as type safety.

My project formalizes a lambda calculus with call/cc using a CEK interpreter described by Matt Might's blog post. Slight modifications were made to allow it to type correctly, but the semantics are very similar.

Building

If you already have Agda installed, compiling src/Project/Cesk.agda should work.

If not, this repository is a Nix flake; simply run nix develop and both neovim with the Agda plugin and VSCode (FOSS edition) with its Agda extension are available in the shell.