article

Denotational semantics of programming languages and compiler generation in PowerEpsilon

Author:

Ming-Yuan ZhuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 36, Issue 9

Pages 39 - 53

https://doi.org/10.1145/609769.609777

Published: 01 September 2001 Publication History

Get Access

Abstract

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.

References

[1]

R. L. Constable and et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc., Englewood Cliffs, New Jersey, 1986.

Digital Library

Google Scholar

[2]

T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2/3), 1988.

Digital Library

Google Scholar

[3]

M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. LNCS 78. Springer-Verlag, 1979.

Google Scholar

[4]

Michael J. C. Gordon. The Denotational Description of Programming Languages, An Introduction. Springer-Verlag, 1979.

Digital Library

Google Scholar

[5]

P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory, Vol. 1. Bibliopolis, Naples, 1984.

Google Scholar

[6]

P. D. Mosses. Compiler generation using denotational semantics. In Mathematical Foundations of Computer Science, volume 45 of Lecture Notes in Computer Science. Springer-Verlag, 1976.

Google Scholar

[7]

J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Mass., 1977.

Digital Library

Google Scholar

[8]

M.-Y. Zhu. AUTOSTAR -- a software development system. ACM SIGPLAN Notices, 24(3), March 1989.

Digital Library

Google Scholar

[9]

M.-Y. Zhu and Y.-Q. Ding. Program extraction by type erasing. Submit to COMPSAC'94, 1994.

Google Scholar

[10]

M.-Y. Zhu and C.-W. Wang. A higher-order lambda calculus: PowerEpsilon. Technical report, Beijing Institute of Systems Engineering, Beijing, 1991.

Google Scholar

[11]

M.-Y. Zhu and C.-W. Wang. Program derivation in PowerEpsilon. In Proceedings of COMPSAC'92, Chicago, September 1992.

Crossref

Google Scholar

Cited By

View all

Luo LZhu M(2003)Partitioning based operating systemACM SIGOPS Operating Systems Review10.1145/881783.88178737:3(23-35)Online publication date: 1-Jul-2003
https://dl.acm.org/doi/10.1145/881783.881787
Zhu M(2001)Formal specifications of debuggersACM SIGPLAN Notices10.1145/609769.60977836:9(54-63)Online publication date: 1-Sep-2001
https://dl.acm.org/doi/10.1145/609769.609778

Index Terms

Denotational semantics of programming languages and compiler generation in PowerEpsilon
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures
    2. Program semantics
      1. Denotational semantics

Recommendations

The denotational semantics of programming languages

This paper is a tutorial introduction to the theory of programming language semantics developed by D. Scott and C. Strachey. The application of the theory to formal language specification is demonstrated and other applications are surveyed. The first ...
Semantics of programming languages

A semantic specification of a programming language can be relevant for programmers to understand software written in the language, as well as for the implementers of a language to understand the intentions of its designers. In the early 1980s, Jan ...
Logic programming semantics: techniques and applications

Comments

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 36, Issue 9

September 2001

73 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/609769

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2001

Published in SIGPLAN Volume 36, Issue 9

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
227
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Luo LZhu M(2003)Partitioning based operating systemACM SIGOPS Operating Systems Review10.1145/881783.88178737:3(23-35)Online publication date: 1-Jul-2003
https://dl.acm.org/doi/10.1145/881783.881787
Zhu M(2001)Formal specifications of debuggersACM SIGPLAN Notices10.1145/609769.60977836:9(54-63)Online publication date: 1-Sep-2001
https://dl.acm.org/doi/10.1145/609769.609778

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

The denotational semantics of programming languages

Semantics of programming languages

Logic programming semantics: techniques and applications

Comments

Published In

Publisher

Publication History

Check for updates

Qualifiers

Other Metrics

Article Metrics

Other Metrics

Cited By

Login options

Full Access

PDF

eReader

Abstract

References

Cited By

Index Terms

Recommendations

The denotational semantics of programming languages

Semantics of programming languages

Logic programming semantics: techniques and applications

Comments

Information

Published In

Publisher

Publication History

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Get Access

Login options

Full Access

View options

PDF

eReader

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations