Proving correctness of compilers using structured graphs

Patrick Bahr

doi:10.1007/978-3-319-07151-0_14

Proving correctness of compilers using structured graphs

Patrick Bahr

Datalogisk Institut

2 Citationer (Scopus)

Abstract

We present an approach to compiler implementation using Oliveira and Cook's structured graphs that avoids the use of explicit jumps in the generated code. The advantage of our method is that it takes the implementation of a compiler using a tree type along with its correctness proof and turns it into a compiler implementation using a graph type along with a correctness proof. The implementation and correctness proof of a compiler using a tree type without explicit jumps is simple, but yields code duplication. Our method provides a convenient way of improving such a compiler without giving up the benefits of simple reasoning.

Originalsprog	Engelsk
Titel	Functional and logic programming : 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings
Antal sider	17
Forlag	Springer
Publikationsdato	2014
Sider	221-237
Kapitel	14
ISBN (Trykt)	978-3-319-07150-3
ISBN (Elektronisk)	978-3-319-07151-0
DOI	https://doi.org/10.1007/978-3-319-07151-0_14
Status	Udgivet - 2014
Begivenhed	International Symposium, FLOPS 2014 - Kanazawa, Japan Varighed: 4 jun. 2014 → 6 jun. 2014 Konferencens nummer: 12

Konference

Konference	International Symposium, FLOPS 2014
Nummer	12
Land/Område	Japan
By	Kanazawa
Periode	04/06/2014 → 06/06/2014

Navn	Lecture notes in computer science
Vol/bind	8475
ISSN	0302-9743

Adgang til dokumentet

10.1007/978-3-319-07151-0_14

Citationsformater

Proving correctness of compilers using structured graphs. / Bahr, Patrick.

Functional and logic programming: 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings. Springer, 2014. s. 221-237 (Lecture notes in computer science, Bind 8475).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Bahr, P 2014, Proving correctness of compilers using structured graphs. i Functional and logic programming: 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings. Springer, Lecture notes in computer science, bind 8475, s. 221-237, International Symposium, FLOPS 2014, Kanazawa, Japan, 04/06/2014. https://doi.org/10.1007/978-3-319-07151-0_14

@inproceedings{d6ad361bb8f54ca8bf5fcb13299491c8,

title = "Proving correctness of compilers using structured graphs",

abstract = "We present an approach to compiler implementation using Oliveira and Cook's structured graphs that avoids the use of explicit jumps in the generated code. The advantage of our method is that it takes the implementation of a compiler using a tree type along with its correctness proof and turns it into a compiler implementation using a graph type along with a correctness proof. The implementation and correctness proof of a compiler using a tree type without explicit jumps is simple, but yields code duplication. Our method provides a convenient way of improving such a compiler without giving up the benefits of simple reasoning.",

author = "Patrick Bahr",

year = "2014",

doi = "10.1007/978-3-319-07151-0_14",

language = "English",

isbn = "978-3-319-07150-3",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "221--237",

booktitle = "Functional and logic programming",

note = "International Symposium, FLOPS 2014 ; Conference date: 04-06-2014 Through 06-06-2014",

}

TY - GEN

T1 - Proving correctness of compilers using structured graphs

AU - Bahr, Patrick

N1 - Conference code: 12

PY - 2014

Y1 - 2014

N2 - We present an approach to compiler implementation using Oliveira and Cook's structured graphs that avoids the use of explicit jumps in the generated code. The advantage of our method is that it takes the implementation of a compiler using a tree type along with its correctness proof and turns it into a compiler implementation using a graph type along with a correctness proof. The implementation and correctness proof of a compiler using a tree type without explicit jumps is simple, but yields code duplication. Our method provides a convenient way of improving such a compiler without giving up the benefits of simple reasoning.

AB - We present an approach to compiler implementation using Oliveira and Cook's structured graphs that avoids the use of explicit jumps in the generated code. The advantage of our method is that it takes the implementation of a compiler using a tree type along with its correctness proof and turns it into a compiler implementation using a graph type along with a correctness proof. The implementation and correctness proof of a compiler using a tree type without explicit jumps is simple, but yields code duplication. Our method provides a convenient way of improving such a compiler without giving up the benefits of simple reasoning.

U2 - 10.1007/978-3-319-07151-0_14

DO - 10.1007/978-3-319-07151-0_14

M3 - Article in proceedings

SN - 978-3-319-07150-3

T3 - Lecture notes in computer science

SP - 221

EP - 237

BT - Functional and logic programming

PB - Springer

T2 - International Symposium, FLOPS 2014

Y2 - 4 June 2014 through 6 June 2014

ER -