"Extracting a formally verified, fully executable compiler from a proof ..."

Stefan Berghofer, Martin Strecker (2003)
a service of Schloss Dagstuhl - Leibniz Center for Informatics