michael/cek-call-cc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
No description
18 commits 1 branch 0 tags 110 KiB
Agda 43.4%
TeX 35.3%
Nix 17.8%
Makefile 3.5%
Find a file
Michael Zhang 99e5df522d vendored
2024-11-12 01:48:57 -06:00
nix Add Nix files + README 2021-12-09 08:21:09 -06:00
src/Project Uncommitted changes 2022-02-02 01:25:03 -06:00
.gitattributes vendored 2024-11-12 01:48:57 -06:00
.gitignore Move source code here. 2021-12-08 00:33:28 -06:00
agda-project.agda-lib More updates to presentation 2021-12-09 07:57:49 -06:00
cesk.png Move source code here. 2021-12-08 00:33:28 -06:00
flake.lock Add Nix files + README 2021-12-09 08:21:09 -06:00
flake.nix Add Nix files + README 2021-12-09 08:21:09 -06:00
main.tex Uncommitted changes 2022-02-02 01:25:03 -06:00
Makefile Uncommitted changes 2022-02-02 01:25:03 -06:00
PragmataPro.ttf More updates to presentation 2021-12-09 07:57:49 -06:00
README.md Add Nix files + README 2021-12-09 08:21:09 -06:00

README.md

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.