Denotational semantics of programming languages and compiler generation in PowerEpsilon

被引：0
作者：
Zhu, MY [1 ]
机构：
[1] CoreTek Syst, Beijing 100086, Peoples R China
来源：
ACM SIGPLAN NOTICES | 2001年 / 36卷 / 09期
关键词：
D O I：
10.1145/609769.609777
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：39 / 53
页数：15
相关论文
共 50 条
12345