school
/
csci8980-s22
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
16 Commits 1 Branch 0 Tags 112 KiB
Vim Script 54.3%
Agda 18.9%
TeX 15.4%
Nix 9.9%
Makefile 1.5%
Go to file
Michael Zhang 2de7a49042
Uncommitted changes 		2022-02-02 01:25:03 -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
.gitignore Move source code here. 2021-12-08 00:33:28 -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
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

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.