A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences

• Paper
• Slides
• Coqdoc
• Sources
• Examples