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][textbook].

[textbook]: https://plfa.github.io/

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][might-cesk]. 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.

[might-cesk]: https://matt.might.net/articles/cesk-machines/