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 条

[1] DENOTATIONAL SEMANTICS OF PROGRAMMING LANGUAGES
TENNENT, RD
COMMUNICATIONS OF THE ACM, 1976, 19 (08) : 437 - 453
[2] TRANSFORMATIONS OF DENOTATIONAL SEMANTICS IN SEMANTICS DIRECTED COMPILER GENERATION
ROYER, V
SIGPLAN NOTICES, 1986, 21 (07): : 68 - 73
[3] DENOTATIONAL SEMANTICS OF PARALLEL PROGRAMMING-LANGUAGES
BREZANY, P
KYBERNETIKA, 1983, 19 (03) : 248 - 262
[4] PROGRAMMING DENOTATIONAL SEMANTICS
ALLISON, L
COMPUTER JOURNAL, 1983, 26 (02): : 164 - 174
[5] DENOTATIONAL SEMANTICS OF QUERY LANGUAGES
SUBIETA, K
INFORMATION SYSTEMS, 1987, 12 (01) : 69 - 82
[6] An Introduction to metric semantics: operational and denotational models for programming and specification languages
van Breugel, F
THEORETICAL COMPUTER SCIENCE, 2001, 258 (1-2) : 1 - 98
[7] Denotational semantics for programming languages, balanced quasi-metrics and fixed points
Rodriguez-Lopez, J.
Romaguera, S.
Valero, O.
INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, 2008, 85 (3-4) : 623 - 630
[8] PROGRAMMING DENOTATIONAL SEMANTICS .2.
ALLISON, L
COMPUTER JOURNAL, 1985, 28 (05): : 480 - 486
[9] Equivalence of Denotational and Operational Semantics for Interaction Languages
Mahe, Erwan
Gaston, Christophe
Le Gall, Pascale
THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 113 - 130
[10] A framework for programming denotational semantics in C++
Papaspyrou, NS
ACM SIGPLAN NOTICES, 1996, 31 (08) : 16 - 25

← 1 2 3 4 5 →