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

Functional metatheory #2

Open

3 of 4 tasks

palmskog opened this issue Jan 23, 2024 · 1 comment

Assignees

Collaborator

palmskog commented Jan 23, 2024 •

edited by Aqissiaq

Loading

Goal: prove type preservation

fill in FIXME
change from Program to Equations
add some arithmetic/bool operations to make the language more interesting
do the type preservation proof

palmskog assigned Aqissiaq

Aqissiaq mentioned this issue

subst and fresh (with wf!) #7

Merged

Aqissiaq mentioned this issue

Type preservation #11

Merged

Collaborator Author

palmskog commented Mar 15, 2024

Full Qed is solved by #15, but probably we want to document the proof in the pdf a bit as well.

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