By the same authors

From the same journal

From the same journal

An algebraic approach to the design of compilers for object-oriented languages

Research output: Contribution to journalArticle



Publication details

JournalFormal Aspects of Computing
DatePublished - 2010
Issue number5
Number of pages47
Pages (from-to)489-535
Original languageEnglish


In this paper we describe an algebraic approach to construct provably correct compilers for object-oriented languages; this is illustrated for programs written in a language similar to a sequential subset of Java. It includes recursive classes, inheritance, dynamic binding, recursion, type casts and test, assignment, and class-based visibility, but a copy semantics. In our approach, we tackle the problem of compiler correctness by reducing the task of compilation to that of program refinement. Compilation is identified with the reduction of a source program to a normal form that models the execution of object code. The normal form is generated by a series of correctness-preserving transformations that are proved sound from the basic laws of the language; therefore it is correct by construction. The main advantages of our approach are the characterisation of compilation within a uniform framework, where comparisons and translations between semantics are avoided, and the modularity and extensibility of the resulting compiler.

    Research areas

  • Algebraic transformation, Refinement, Compiler correctness, REFINEMENT ALGEBRA, COMPILATION, MODEL, UTP

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations