Modular Denotational Semantics for Compiler Construction

Authors:

Sheng Liang and Paul Hudak

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.

Bibtex:

 @InProceedings{liang-hudak:modular-semantics,
  author =      "Sheng Liang and Paul Hudak",
  title =       "Modular Denotational Semantics for Compiler Construction",
  booktitle =   "Proc. European Symposium on Programming",
  year =        "1996",
  month =       "April",
  pages =       "219--234",
  publisher =   "Springer-Verlag"
} 

Links:

ESOP-MonInterp.pdf