Denotational semantics of programming languages and compiler generation in PowerEpsilon
Ming-Yuan Zhu · ACM SIGPLAN Notices · 2001
Programming in constructive type theory corresponds to theorem proving in mathematics: the specification plays the role of the proposition to be proved and the program is obtained from the proof. In this paper, we present an approach of using constructive type theory to derive a compiler of a given programming language from its denotational semantic definition. The development is supported by a proof development system called PowerEpsilon .