osa1 feed

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:

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 …