New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Finish LambdaANF Correctness Proof #111

Open

mattam82 opened this issue Jan 27, 2025 · 1 comment

Assignees

Collaborator

mattam82 commented Jan 27, 2025

Figure out what's missing and try to split it in self-contained subgoals

mattam82 assigned zoep

mattam82 moved this to Todo in Cleanups and Improvements

mattam82 added this to Cleanups and Improvements

Member

zoep commented Jan 27, 2025

There two way we can go about this:

Verify the already existing ANF transformation from lambdaBox
Write a CPS -> direct style transformation in the λANF backend and prove it correct with the logical relation framework.

2 may make the proof easier, but we keep around the CPS transformation that may not be useful.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment