A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences
Paper
Slides
Coqdoc
Sources
Examples