π: Towards a Simple Formal Semantic Framework for Compiler Construction

被引：0
|
作者：
Braga, Christiano [1 ,2 ]
机构：
[1] Univ Fed Fluminense, Inst Comp, Niteroi, RJ, Brazil
[2] Univ Complutense Madrid, FADoSS Res Grp, Madrid, Spain
来源：
SAC '19: PROCEEDINGS OF THE 34TH ACM/SIGAPP SYMPOSIUM ON APPLIED COMPUTING | 2019年
关键词：
Program semantics; Program reasoning; Compilers; MODULAR REWRITING SEMANTICS;
D O I：
10.1145/3297280.3299740
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
Compiler construction is considered an intimidating discipline in Computer Science and related courses. This is perhaps captured quite graphically by the cover of the standard book on the subject, the so-called "Dragon book", by Alfred V. Aho, Jeffrey D. Ullman and later on with Ravi Sethi and Monica S. Lam. There are "red", "green" and "purple dragon" editions, but the Dragon, representing how burdensome people think of the subject, is always there. The aim of this paper is to introduce pi, a formal semantic framework for compiler construction together with program validation and its implementation in the Maude language that aims at easing the process of compiler construction in a rigorous way.
引用
收藏
页码：1562 / 1569
页数：8
相关论文
共 50 条
  • [31] Towards a Unifying Framework for Formal Theories of Novelty
    Boult, T. E.
    Grabowicz, P. A.
    Prijatelj, D. S.
    Stern, R.
    Holder, L.
    Alspector, J.
    Jafarzadeh, M.
    Ahmad, T.
    Dhamija, A. R.
    Li, C.
    Cruz, S.
    Shrivastava, A.
    Vondrick, C.
    Scheirer, W. J.
    THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 15047 - 15052
  • [32] Towards a Formal Framework of Vulnerability to Climate Change
    Cezar Ionescu
    Richard J. T. Klein
    Jochen Hinkel
    K. S. Kavi Kumar
    Rupert Klein
    Environmental Modeling & Assessment, 2009, 14 : 1 - 16
  • [33] Formal verification of an optimizing compiler
    Leroy, Xavier
    MEMOCODE'07: FIFTH ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2007, : 25 - 25
  • [34] Formal Verification of a Realistic Compiler
    Leroy, Xavier
    COMMUNICATIONS OF THE ACM, 2009, 52 (07) : 107 - 115
  • [35] FORMAL SPECIFICATION OF A PROLOG COMPILER
    HANUS, M
    LECTURE NOTES IN COMPUTER SCIENCE, 1989, 348 : 273 - 282
  • [36] Formal verification of an optimizing compiler
    Leroy, Xavier
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2007, 4533 : 1 - 1
  • [37] Towards the formal verification of a C0 compiler: Code generation and implementation correctness
    Leinenbach, D
    Paul, W
    Petrova, E
    SEFM 2005: THIRD IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2005, : 2 - 11
  • [38] FRAMEWORK FOR SEMANTIC RECONCILIATION OF CONSTRUCTION PROJECT INFORMATION
    Mutis, Ivan
    Issa, Raja R. A.
    JOURNAL OF INFORMATION TECHNOLOGY IN CONSTRUCTION, 2012, 17 : 1 - 24
  • [39] K: A Semantic Framework for Programming Languages and Formal Analysis Tools
    Rosu, Grigore
    DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2017, 50 : 186 - 206
  • [40] A Framework for the composition and formal verification of adaptable semantic Web services
    Ben Lamine, Rihab
    Ben Djemaa, Raoudha
    Amous, Ikram
    16TH INTERNATIONAL CONFERENCE ON ADVANCES IN MOBILE COMPUTING AND MULTIMEDIA (MOMM 2018), 2014, : 25 - 33
12345