Proving soundness of simply typed multi-staged lambda-calculus

March 6, 2014 - Tagged as: en, coq, plt, multi-stage programming.

First part of my first non-trivial(e.g. something other than a Software Foundations exercise) Coq program is finally done. I learned Coq from Software Foundations, but I didn’t finish to book. I still know only very basic tactics, which I think is one of the reasons why my proofs are so long. You can see the source here.

Some random notes about implementation:

• I’m looking to improve proofs. I have a lot more to implement for the rest of the program until deadline, so I may not be able to refactor current proofs very much, but at one point I want to simplify the proofs and use more advanced tactics.
• Currently only inversion, destruct, induction, rewrite, assumption, assert, constructor, auro, simpl, intro/intros, apply, right/left, exists, unfold, subst, reflexivity, remember and generalize tactics are used.
• Language definition is almost the same as in papers. There is one difference, we implemented substitutions as a function. In reality, substitution in multi-staged lambda-calculus is not a function. I believe this doesn’t effect correctness of theorems. At one point I’ll refactor the code and define substitution as a relation.
• I used Case, SCase, SSCase … constructs from SFlib extensively.

Now I’m going to implement lambda-calculus with row-polymorphic records. I expect this to be at least 2x harder, since polymorphism is involved. Let’s see how it goes …

---