article

Free access

Program transformation in constructive type theory

Author:

Ming-Yuan ZhuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 30, Issue 1

Pages 11 - 19

https://doi.org/10.1145/199818.199833

Published: 03 January 1995 Publication History

PDF eReader

Abstract

Transformational programming is a method for program development. To formalize the transformational programming techniques, the key point is to formally represent transformation rules and to prove the correctness of these rules. In this paper, we describe a constructive type-theoretical approach for formalizing the concepts of program schema, transformation rules and strategies, and software development processes. Some examples for verification and derivation of semantically correct program transformation rules are presented.

References

[1]

[Barz 77] Barzdin, J.M.: "Inductive Inference of Automata, Functions and Programs", Amer. Math. Soc. Translations, Vol. 109, No. 2, 1977.

Google Scholar

[2]

[Blum 75] Blum, L. and Blum, M.: "Toward a Mathematical Theory of Inductive Inference", Information Control, Vol. 28, 1975.

Crossref

Google Scholar

[3]

[BierBP 75] Biermann, A.W., Baum, R.I. and Petry, F.E.: "Speeding up the Synthesis of Programs from Traces", IEEE Transactions on Computers, Vol. C-24, No. 2, 1975.

Google Scholar

[4]

[BierK 76] Biermann, A.W. and Krishnaswamy, R.: "Constructing Programs from Example Computations", IEEE Transactions on Software Engineering, Vol. SE-2, 1976.

Digital Library

Google Scholar

[5]

[Gold 67] Gold, M.: "Languge Identification in the Limit", Information Control, Vol. 5, 1967.

Google Scholar

[6]

[Zhu 89] Zhu, M.-Y.: "AUTOSTAR - A Software Development System", ACM SIGPLAN Notices, Vol. 24, No. 3, March, 1989.

Digital Library

Google Scholar

[7]

[ZhuW 91] Zhu, M.-Y. and Wang, C.-W.: "A Higher-Order Lambda Calculus: PowerEpsilon", Technical Report, Beijing Institute of Systems Engineering, Beijing, 1991.

Google Scholar

[8]

[ZhuW 92] Zhu, M.-Y. and Wang, C.-W.: "Program Derivation in PowerEpsilon", Proceedings of COMPSAC'92, Chicago, September, 1992.

Crossref

Google Scholar

Index Terms

Program transformation in constructive type theory
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Type-changing rewriting and semantics-preserving transformation
PEPM '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation

We have identified a class of regular, whole-program transformations that cannot be safely performed with typical transformation techniques because transformation requires changing the types of terms. In these transformations, we want to change ...
Type-safe two-level data transformation
FM'06: Proceedings of the 14th international conference on Formal Methods

A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. Examples of two-level data transformations include XML schema evolution ...
Point-free Program Transformation
Program Transformation: Theoretical Foundations and Basic Techniques. Part 1

Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 30, Issue 1

Jan. 1995

57 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/199818

Editor:
Richard L. Wexelblat
IRS IS:AO, Washington, DC

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 January 1995

Published in SIGPLAN Volume 30, Issue 1

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
106
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)3

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Abstract

References

Index Terms

Recommendations

Type-changing rewriting and semantics-preserving transformation

Type-safe two-level data transformation

Point-free Program Transformation

Comments

Information

Published In

Publisher

Publication History

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations