Specification, verification and prototyping of an optimized compiler
scientific article; zbMATH DE number 741023