Resugaring: Lifting Evaluation Sequences through Syntactic Sugar
Justin Pombrio and Shriram Krishnamurthi
The paper: resugar.pdf
The source code for Confection: confection.zip. (This is a snapshot of the brownplt/Resugarer repository on Github. The README is in the zipfile.)
Partial proofs in Coq: coq.tgz. These are also available in the Confection repo above.
The source code for Pyret with Confection attached is available on Github: brownplt/pyret-lang-resugarer.