kth-step / abs-metatheory

https://kth-step.github.io/abs-metatheory
MIT License
0 stars 0 forks source link

Functional metatheory #2

Open palmskog opened 9 months ago

palmskog commented 9 months ago

Goal: prove type preservation

palmskog commented 8 months ago

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