Skip to main content
SpringerLink
Log in

Uniform traversal combinators: Definition, use and properties

  • Conference paper
  • First Online:
Automated Deduction—CADE-11 (CADE 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 607))

Included in the following conference series:

Abstract

In this paper we explore ways of capturing well-formed patterns of recursion in the form of generic reductions. These reductions, called uniform traversal combinators, can substantially help the theorem proving process by eliminating the need for induction and can also be an aid in achieving effective program synthesis.

This paper is based on work supported by the National Science Foundation under grants IRI-8606424 and IRI 8822121 and by the Office of Naval Research University Research Initiative contract, number N00014-86-K-0764

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. S. Bird. The Promotion and Accumulation Strategies in Transformational Programming. ACM Transactions on Programming Languages and Systems, 6(4):487–504, October 1984.

    Google Scholar 

  2. C. Bohm and A. Berarducci. Automatic Synthesis of Typed A-Programs on Term Algebras. Theoretical Computer Science, 39:135–154, 1985.

    Google Scholar 

  3. R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979.

    Google Scholar 

  4. L. Fegaras, T. Sheard, and D. Stemple. The ADABTPL Type System. In Proceedings of the Second International Workshop on Database Programming Languages, Salishan, Oregon, pages 243–254, 1989.

    Google Scholar 

  5. C. A. Hoare. Recursive Data Structures. Journal of the ACM, 4(2):105–132, June 1975.

    Google Scholar 

  6. P. Hudak. Conception, Evolution, and Application of Functional Programming Languages. ACM Computing Surveys, 21(3):359–411, September 1989.

    Google Scholar 

  7. N. Immerman, S. Patnaik, and D. Stemple. The Expressiveness of a Family of Finite Set Languages. Proceedings of the Tenth ACM Symposium on Principles of Database Systems, Denver, Colorado, pages 37–52, May 1991.

    Google Scholar 

  8. G. Malcolm. Homomorphisms and Promotability. In Mathematics of Program Construction, pages 335–347. Springer-Verlag, June 1989.

    Google Scholar 

  9. E. Meijer, M. Fokkinga, and R. Paterson. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. In fifth ACM Conference on Functional Programming Languages and Computer Architecture, Cambridge Massachusetts, pages 124–144, August 1991.

    Google Scholar 

  10. H. Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.

    Google Scholar 

  11. T. Sheard. Generalized Recursive Structure Combinators. Technical report, University of Massachusetts at Amherst, 1989. COINS Technical Report 89-26.

    Google Scholar 

  12. T. Sheard. Automatic Generation and Use of Abstract Structure Operators. ACM Transactions on Programming Languages and Systems, 19(4):531–557, October 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Massachusetts, 01003, Amherst, MA

    Leonidas Fegaras & David Stemple

  2. Department of Computer Science and Engineering, Oregon Graduate Institute, 97006, Beaverton, OR

    Tim Sheard

Authors
  1. Leonidas Fegaras
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tim Sheard
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Stemple
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fegaras, L., Sheard, T., Stemple, D. (1992). Uniform traversal combinators: Definition, use and properties. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_162

Download citation

  • DOI: https://doi.org/10.1007/3-540-55602-8_162

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55602-2

  • Online ISBN: 978-3-540-47252-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation