dyniec/mgr
1
Fork 0
Code Activity Actions
No description
119 commits 2 branches 0 tags 4.5 MiB
  • TeX 88.3%
  • Makefile 5.6%
  • Nix 4.9%
  • Lua 1.2%
Find a file
Exact
Paweł Dybiec 1e28411d13
Some checks failed
/ agda (push) Failing after 34s
Details
/ pdf (push) Successful in 4m42s
Details
readme
2026-03-20 18:00:07 +01:00
.forgejo/workflows Build pdf with nix 2026-02-17 20:10:27 +01:00
mgr final fixes 2026-03-12 16:53:12 +01:00
pandoc Doc base 2026-02-17 03:19:10 +01:00
.envrc direnv 2025-12-18 00:46:05 +01:00
.gitignore type abstraction and substitution 2026-01-26 01:58:51 +00:00
bibitems.tex intro 2026-03-12 13:49:29 +01:00
doc.pdf final fixes 2026-03-12 16:53:12 +01:00
doc.tex final fixes 2026-03-12 16:53:12 +01:00
flake.lock nix 2025-12-17 21:20:56 +01:00
flake.nix Build pdf with nix 2026-02-17 20:10:27 +01:00
iithesis.cls Doc base 2026-02-17 03:19:10 +01:00
Makefile abstract and types 2026-02-17 18:51:07 +01:00
mgr.agda-lib types 2025-12-16 03:05:09 +01:00
README.md readme 2026-03-20 18:00:07 +01:00

README.md

Verified compiler for a language with control effects

Despite the title there's no compiler, as I didn't manage to complete it in time before thesis defence. This work presents formalisation of a calculus with multiprompt shift0 and reset0 with first class labels. Formalisation work is done in Agda, though there's few holes in proofs and few postulates.