Write your Compiler by Proving it Correct - 23rd August, 2015 Context splitting and substructural terms - 1st January 2014