Я ищу учебный материал, который охватывает доказательства корректности компилятора, предпочтительно с использованием денотационных методов, на уровне начинающего аспиранта.
В качестве альтернативы, вы знаете несколько простых примеров компилятора, которые я мог бы использовать для иллюстрации проблем? (Первым примером, который мне пришёл в голову, был переводчик с выражений из инфикса в постфикс. Но он не смог показать ничего интересного, кроме как сделать индукцию по синтаксису.)
У Грэма Хаттона есть небольшой пример в его книге «Программирование на Хаскеле», который является отличным местом для начала.
У меня также есть несколько механизированных доказательств (различные логики) компилятора McCarthy-Painter в отчете, который я сделал для моей докторской диссертации .
источник
Возможно, это не самый простой пример, но Ксавье Леруа проделал большую работу в этой области, например, официально проверенный компилятор Си . Он провел презентацию в летней школе с использованием небольшого императивного языка IMP, который является доступным введением в более продвинутую работу.
источник