Provas de correção do compilador

Estou procurando um material tutorial que cubra as provas de correção do compilador, de preferência usando métodos denotacionais, no nível de um estudante iniciante.

Como alternativa, você conhece alguns exemplos simples de compilador que eu poderia usar para ilustrar os problemas? (O primeiro exemplo que me ocorreu foi um tradutor de expressões infix para postfix. Mas não mostrou nada de interessante além de como fazer indução na sintaxe.)

Não conheço um bom material tutorial, mas há trabalhos que são suficientemente elementares para um estudante de graduação (como eu). O primeiro pode ser o que você está procurando (a ênfase é minha).

Provas simples de correção relacional para análises estáticas e transformações de programas , Nick Benton. 2004.

Mostramos como algumas análises estáticas clássicas para programas imperativos e as transformações otimizadoras que eles possibilitam podem ser expressas e provadas corretas usando técnicas lógicas e denotacionais elementares . Os principais ingredientes são uma interpretação das propriedades do programa como relações, em vez de predicados, e uma constatação de que, embora muitas análises de programas sejam tradicionalmente formuladas em termos muito intensivos, as transformações associadas são realmente possibilitadas por propriedades extencionais mais liberais.

Esses documentos também podem lhe interessar. Eles me ajudaram muito!

1. Provando a correção das otimizações do compilador por lógica temporal , David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. Eu teria pensado que havia mais material usando bisimulação no contexto de otimizações do compilador. Se seu objetivo é realmente técnicas denotacionais, você provavelmente pode codificar essas provas usando caracterizações de bisimulação.
2. Gerando otimizações de compilador a partir de provas , Ross Tate, Michael Stepp e Sorin Lerner. Inclui uma formalização teórica por categoria de seu método de prova.
3. Provando otimizações corretas usando a equivalência de programa parametrizada , Sudipta Kundu, Zachary Tatlock e Sorin Lerner. Vá lá se você gosta de relações lógicas.
4. Um back-end do compilador formalmente verificado Xavier Leroy.

Você precisará modernizar a notação, mas a correção de McCarthy e Painter de um compilador para expressões aritméticas é simples, boa e também de interesse histórico (já que, até onde sei, é o primeiro artigo sobre o assunto).

Um compilador de preservação de tipo certificado de Adam Chlipala, do Lambda Calculus para Assembly Language, parece ser um bom exemplo de uma simples prova de correção do compilador usando métodos denotacionais, com a vantagem adicional de ter sido formalizada completamente em um assistente de prova.

Graham Hutton tem um pequeno exemplo em seu livro "Programming in Haskell", que é um ótimo lugar para começar.

Também tenho algumas provas mecanizadas (várias lógicas) do compilador McCarthy-Painter em um relatório que fiz para meu doutorado .

Talvez não seja o exemplo mais simples, mas Xavier Leroy fez muito trabalho nessa área, como um compilador C formalmente verificado . Ele fez uma apresentação na escola de verão usando uma pequena linguagem imperativa IMP, que é uma introdução acessível ao trabalho mais avançado.