Bukti kebenaran kompiler

Saya mencari materi tutorial yang mencakup bukti kebenaran kompiler, lebih disukai menggunakan metode denotasi, pada tingkat siswa lulusan awal.

Atau, apakah Anda tahu beberapa contoh kompiler sederhana yang dapat saya gunakan untuk menggambarkan masalah? (Contoh pertama yang terpikir oleh saya adalah penerjemah dari infix ke ekspresi postfix. Tetapi gagal menunjukkan hal yang menarik selain bagaimana melakukan induksi pada sintaks.)

Saya tidak tahu materi tutorial yang baik, tetapi ada makalah yang cukup dasar untuk mahasiswa pascasarjana (seperti saya). Yang pertama mungkin apa yang Anda cari (penekanan adalah milikku).

Bukti kebenaran relasional sederhana untuk analisis statis dan transformasi program , Nick Benton. 2004

Kami menunjukkan bagaimana beberapa analisis statis klasik untuk program-program penting, dan transformasi optimal yang dimungkinkannya, dapat diekspresikan dan dibuktikan benar dengan menggunakan teknik-teknik logis logis dan denotasional . Bahan-bahan utama adalah interpretasi sifat-sifat program sebagai hubungan, bukan predikat, dan kesadaran bahwa meskipun banyak analisis program secara tradisional dirumuskan dalam istilah yang sangat intens, transformasi terkait sebenarnya dimungkinkan oleh sifat ekstensional yang lebih liberal.

Makalah ini mungkin juga menarik bagi Anda. Mereka sangat membantu saya!

1. Membuktikan kebenaran optimasi kompiler oleh Logika Temporal , David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen. Saya akan berpikir ada lebih banyak bahan menggunakan bisimulasi dalam konteks optimisasi kompiler. Jika tujuan Anda benar-benar teknik denotasional, Anda mungkin dapat menyandikan bukti-bukti ini menggunakan karakterisasi bisimulasi.
2. Menghasilkan Optimalisasi Kompiler dari Bukti , Ross Tate, Michael Stepp, dan Sorin Lerner. Termasuk formalisasi teori kategori metode pembuktian mereka.
3. Proving Optimization Benar menggunakan Parameter Program Kesetaraan , Sudipta Kundu, Zachary Tatlock, dan Sorin Lerner. Pergi ke sana jika Anda suka hubungan logis.
4. Kompilator Back-end Resmi Xavier Leroy yang Diverifikasi Secara Resmi .

Anda perlu memodernisasi notasi, tetapi Ketepatan Kompiler untuk Ekspresi Aritmatika McCarthy dan Painter sederhana dan bagus, dan juga menarik secara historis (karena sepengetahuan saya ini adalah makalah pertama tentang masalah ini).

Kompiler Preserving Tipe-Certified Adam Chlipala dari Lambda Calculus ke Assembly Language tampaknya menjadi contoh yang baik dari bukti ketepatan kompilator sederhana menggunakan metode denotasional, dengan keuntungan tambahan karena telah diformalkan sepenuhnya dalam asisten bukti.

Graham Hutton memiliki contoh kecil dalam bukunya "Programming in Haskell" yang merupakan tempat yang tepat untuk memulai.

Saya juga memiliki beberapa bukti mekanis (berbagai logika) dari kompiler McCarthy-Painter dalam laporan yang saya lakukan untuk PhD saya .

Mungkin bukan contoh paling sederhana, tetapi Xavier Leroy telah melakukan banyak pekerjaan di bidang ini, seperti kompiler C yang terverifikasi secara formal . Dia memberikan presentasi sekolah musim panas menggunakan IMP bahasa imperatif kecil, yang merupakan pengantar diakses untuk pekerjaan yang lebih maju.