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

Department of Computer Science

2 Citations (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.

Original language	English
Title of host publication	Functional and logic programming : 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings
Number of pages	17
Publisher	Springer
Publication date	2014
Pages	221-237
Chapter	14
ISBN (Print)	978-3-319-07150-3
ISBN (Electronic)	978-3-319-07151-0
DOIs	https://doi.org/10.1007/978-3-319-07151-0_14
Publication status	Published - 2014
Event	International Symposium, FLOPS 2014 - Kanazawa, Japan Duration: 4 Jun 2014 → 6 Jun 2014 Conference number: 12

Conference

Conference	International Symposium, FLOPS 2014
Number	12
Country/Territory	Japan
City	Kanazawa
Period	04/06/2014 → 06/06/2014

Series	Lecture notes in computer science
Volume	8475
ISSN	0302-9743

Access to Document

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

Cite this

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. p. 221-237 (Lecture notes in computer science, Vol. 8475).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Bahr, P 2014, Proving correctness of compilers using structured graphs. in Functional and logic programming: 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings. Springer, Lecture notes in computer science, vol. 8475, pp. 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 -