%0 Unpublished Work %1 Meijer94 %A Meijer, Erik %D 1994 %K Squiggol applic.CP compiler directed divers.denot generation, semantics %T More Advice on Proving Compilers Correct: Improve Correct Compilers %U http://www.cs.ruu.nl/\~erik/advice.html %X As an alternative to the classical approach to the compiler correctness problem where a given compiler is proved correct from scratch, we propose a method for deriving correct compilers from a denotational semantics via a series of refinements. Each such optimization step corresponds to an efficiency improvement in the corresponding compiler. Our technique combines the standard initial algebra semantics approach with aspects of Action Semantics. Instead of expressing semantic functions as homomorphisms from the initial algebra (syntax) to some semantic domain, they are factored through an algebra of actions. Compilers can then be obtained by viewing semantic functions as translations from the source language to the initial action algebra. We illustrate our method by deriving several compilers for a language of arithmetic expressions. Though simple, this example shows all the steps necessary to deal with more realistic languages.

@unpublished{Meijer94, abstract = {As an alternative to the classical approach to the compiler correctness problem where a given compiler is proved correct from scratch, we propose a method for deriving correct compilers from a denotational semantics via a series of refinements. Each such optimization step corresponds to an efficiency improvement in the corresponding compiler. Our technique combines the standard initial algebra semantics approach with aspects of Action Semantics. Instead of expressing semantic functions as homomorphisms from the initial algebra (syntax) to some semantic domain, they are factored through an algebra of actions. Compilers can then be obtained by viewing semantic functions as translations from the source language to the initial action algebra. We illustrate our method by deriving several compilers for a language of arithmetic expressions. Though simple, this example shows all the steps necessary to deal with more realistic languages.}, added-at = {2009-05-10T18:36:57.000+0200}, author = {Meijer, Erik}, biburl = {https://www.bibsonomy.org/bibtex/2a9a90216511d97e7b22a3bc5e550ebd9/dparigot}, description = {Attribute Grammar}, interhash = {7c4936d68deb79c2fe18e0a54b0d4cc2}, intrahash = {a9a90216511d97e7b22a3bc5e550ebd9}, keywords = {Squiggol applic.CP compiler directed divers.denot generation, semantics}, month = {September}, postscript = {http://www.cs.ruu.nl/\~erik/advice.ps}, scope = {tools}, timestamp = {2009-05-10T18:37:05.000+0200}, title = {More Advice on Proving Compilers Correct: Improve Correct Compilers}, url = {http://www.cs.ruu.nl/\~erik/advice.html}, year = 1994 }