Modular Denotational Semantics for Compiler Construction Export

@inproceedings{citeulike:4746704, abstract = {. We show the benefits of applying modular monadic semantics to compiler construction. Modular monadic semantics allows us to define a language with a rich set of features from reusable building blocks, and use program transformation and equational reasoning to improve code. Compared to denotational semantics, reasoning in monadic style offers the added benefits of highly modularized proofs and more widely applicable results. To demonstrate, we present an axiomatization of environments, and use it to prove the correctness of a well-known compilation technique. The monadic approach also facilitates generating code in various target languages with different sets of built-in features. 1 Introduction We propose a modular semantics which allows language designers to add (or remove) programming language features without causing global changes to the existing specification, derive a compilation scheme from semantic descriptions, prove the correctness of program transformation and compilation...}, author = {Liang, Sheng and Hudak, Paul}, booktitle = {In European Symposium on Programming}, citeulike-article-id = {4746704}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7816}, keywords = {compilers, dsl, monad-transformers, monads}, pages = {219--234}, posted-at = {2009-06-04 22:10:22}, priority = {4}, title = {Modular Denotational Semantics for Compiler Construction}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7816}, volume = {1058}, year = {1996} }

TY - CONF ID - citeulike:4746704 L3 - citeulike-article-id:4746704 N2 - . We show the benefits of applying modular monadic semantics to compiler construction. Modular monadic semantics allows us to define a language with a rich set of features from reusable building blocks, and use program transformation and equational reasoning to improve code. Compared to denotational semantics, reasoning in monadic style offers the added benefits of highly modularized proofs and more widely applicable results. To demonstrate, we present an axiomatization of environments, and use it to prove the correctness of a well-known compilation technique. The monadic approach also facilitates generating code in various target languages with different sets of built-in features. 1 Introduction We propose a modular semantics which allows language designers to add (or remove) programming language features without causing global changes to the existing specification, derive a compilation scheme from semantic descriptions, prove the correctness of program transformation and compilation... EP - 234 TI - Modular Denotational Semantics for Compiler Construction VL - 1058 T2 - In European Symposium on Programming SP - 219 KW - compilers KW - dsl KW - monad-transformers KW - monads AU - Liang, Sheng AU - Hudak, Paul PY - 1996/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7816 ER -