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 条
  • [21] A FORMAL SEMANTICS FOR COMPUTER LANGUAGES AND ITS APPLICATION IN A COMPILER-COMPILER
    FELDMAN, JA
    COMMUNICATIONS OF THE ACM, 1966, 9 (01) : 3 - &
  • [22] Denotational and operational semantics for interaction languages: Application to trace analysis
    Mahe, Erwan
    Gaston, Christophe
    Le Gall, Pascale
    SCIENCE OF COMPUTER PROGRAMMING, 2024, 232
  • [23] Auto-compiler of programming languages
    Qin, Zhensong
    Fan, Bonan
    Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 1997, 34 (03): : 212 - 216
  • [24] Investigating Push-out Properties in the Category of Riesz Modules: A Study on Denotational Semantics in probabilistic Programming Languages
    Maihemuti, Nueraminaimu
    Liu, Jiyu
    Tang, Jiangang
    Yu, Xiaowen
    PROCEEDINGS OF 2024 INTERNATIONAL CONFERENCE ON COMPUTER AND MULTIMEDIA TECHNOLOGY, ICCMT 2024, 2024, : 185 - 189
  • [25] An object-oriented denotational semantics of a small programming language
    Dong, JS
    Duke, R
    Rose, G
    OBJECT ORIENTED SYSTEMS, 1997, 4 (01): : 29 - 52
  • [26] The design of the YAP compiler: An optimizing compiler for logic programming languages
    da Silva, Anderson Faustino
    Costa, Vitor Santos
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2006, 12 (07) : 764 - 787
  • [27] DENOTATIONAL SEMANTICS OF MIXED COMPUTATION PROCESSES FOR A STRUCTURAL PROGRAMMING LANGUAGE
    ZAKHAROVA, NT
    PETRUSHIN, VA
    YUSHCHENKO, EL
    CYBERNETICS, 1988, 24 (01): : 19 - 32
  • [28] COMPILER GENERATION FROM RELATIONAL SEMANTICS
    DAM, M
    JENSEN, F
    LECTURE NOTES IN COMPUTER SCIENCE, 1986, 213 : 1 - 29
  • [29] Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
    Lew, Alexander K.
    Cusumano-Towner, Marco F.
    Sherman, Benjamin
    Carbin, Michael
    Mansinghka, Vikash K.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [30] Automated Test Oracle Generation via Denotational Semantics
    Guo, Hai-Feng
    Cao, Liang
    Song, Yushu
    Qiu, Zongyan
    2014 14TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC 2014), 2014, : 139 - 144
12345