37 lines
1.2 KiB
Markdown
37 lines
1.2 KiB
Markdown
|
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/
|
||
|
|
|