Formal compiler construction in a logical framework
scientific article; zbMATH DE number 5073694