Skip to main content
SpringerLink
Log in

A National Science Foundation Proposal

  • Chapter
Automatic Program Development

  • 316 Accesses

Summary

The objectives of this research are to improve software productivity, reliability, and performance of complex systems. The approach combines program transformations, sometimes in reflective ways, to turn very high-level perspicuous specifications into efficient implementations. These transformations will be implemented in a metatransformational system, which itself will be transformed from an executable specification into efficient code. Experiments will be conducted to assess the research objectives in scaled-up applications targetted to systems that perform complex program analysis and translation.

The transformations to be used include (i) dominated convergence (for implementing fixed-points efficiently), (ii) finite differencing (for replacing costly repeated calculations by less expensive incremental counterparts), (iii) data structure selection (for simulating associative access on a RAM in real time), and (iv) partial evaluation (for eliminating interpretive overhead and simplification). Correctness of these transformations, of user-defined transformations, and of the transformational system itself will be addressed in part. Both the partial evaluator and components of the transformational system that perform inference and conditional rewriting will be derived by transformation from high-level specifications. Other transformations will be specified in terms of Datalog-like inference and conditional rewriting rules that should be amenable to various forms of rule induction.

Previously, Cai and Paige in [12] used an ideal model of productivity free from all human factors in order to demonstrate experimentally how a transformation from a low-level specification language into C could be used to obtain a fivefold increase in the productivity of efficient algorithm implementation in C in comparison to hand-coded C. However, only small-scale examples were considered. The proposed research includes a plan to expand this model of productivity to involve other specification languages (and their transformation to C), and to conduct experiments to demonstrate how to obtain a similar fivefold improvement in productivity for large-scale examples of C programs that might exceed 100,000 lines.

The proposal lays out extensive evidence to support the approach, which will be evaluated together with its theoretical underpinnings through substantial experiments. If successful, the results are expected to have important scientific and economic impact. They are also expected to make interesting, new pedagogical connections between the areas of programming languages, software engineering, databases, artificial intelligence, and algorithms.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Bancilhon: Naive evaluation of recursively defined relations. In On Knowledge-Base Management Systems, M. Brodie and J. Mylopoulos (Eds.). McGraw-Hill, 165–178, 1986.

    Google Scholar 

  2. R. Bayer: Query evaluation and recursion in deductive database system, Unpublished Manuscript, 1985.

    Google Scholar 

  3. B. Bloom: Ready simulation, bisimulation, and the semantics of CCS-like languages. Ph.D. thesis, Massachusetts Institute of Technology, Sept. 1989.

    Google Scholar 

  4. B. Bloom and R. Paige: Transformational design and implementation of a new efficient solution to the ready simulation problem. Science of Computer Programming, 24(3), 189–220, 1995. http://cs.nyu.edu/cs/faculty/paige/papers/readysc.ps.

  5. P. Borras, D. Clement, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual: Centaur: the system. Rapports de Recherche 777, INRIA, 1987.

    Google Scholar 

  6. J. Cai: A language for semantic analysis. Technical Report 635, Courant Institute, New York University, 1993.

    Google Scholar 

  7. J. Cai, P. Facon, F. Henglein, R. Paige, and E. Schonberg: Type transformation and data structure choice. In Constructing Programs From Specifications, B. Möller, (Ed.). North-Holland, Amsterdam, 126–164, 1991.http://cs.nyu.edu/cs/faculty/paige/papers/subtype.ps.

  8. J. Cai and R. Paige: Binding performance at language design time. In Proc. Fourteenth ACM Symp. on Principles of Programming Languages, 85–97 1987.

    Google Scholar 

  9. J. Cai and R. Paige: Program derivation by fixed-point computation. Science of Computer Programming, 11:3, 197–261, 1989.http://cs.nyu.edu/cs/faculty/paige/papers/fixpoint.ps.

  10. J. Cai and R. Paige: Languages polynomial in the input plus output. In Algebraic Methodology and Software Technology, M. Nivat, C. Rattray, T. Rus, and G. Scollo, (Eds.,) Workshops in Computing, Springer-Verlag, Conference Record of the Second AMAST, 287–302, 1992.

    Google Scholar 

  11. J. Cai and R. Paige: Using multiset discrimination to solve language processing problems without hashing. Theoretical Computer Science, 145(1–2), 189–228, 1995. http://cs.nyu.edu/cs/faculty/paige/papers/hash.ps.

  12. Cai J. and R. Paige: Towards increased productivity of algorithm implementation. In Proc. ACM SIGSOFT, 71–78, 1993. http://cs.nyu.edu/cs/faculty/paige/papers/prod.ps.

  13. J. Cai, R. Paige, and R. Tarjan: More efficient bottom-up multi-pattern matching in trees. Theoretical Computer Science, 106(1), 21–60, 1992. http://cs.nyu.edu/pub/tech-reports/tr604.ps.Z.

  14. A. Cantali: Using ETNA to prove correctenss and complexity of a linear time implementation of a subset of Willard’s RCS. Bachelor’s thesis, University of Catania, Catania, Italy, 1997.

    Google Scholar 

  15. C.-H. Chang and R. Paige: From regular expressions to DFA’s using compressed NFA’s. Theoretical Computer Science, 178(1–2), 1–36, 1997. http://cs.nyu.edu/cs/faculty/paige/papers/cnnfa.ps.

  16. P. Cousot and R. Cousot: Constructive versions of Tarski’s fixed-point theorems. Pacific J. Math., 82(1), 43–57, 1979.

    MATH  MathSciNet  Google Scholar 

  17. H. Curry: Modified basic functionality in combinatory logic. Dialectica, 23, 83–92, 1969.

    Article  MATH  Google Scholar 

  18. V. Donzeau-Gouge, G. Huet, G. Kahn, and B. Lang: Programming environments based on structured editors: The mentor experience. In Interactive Programming Environments. McGraw-Hill, 1984.

    Google Scholar 

  19. W. Dowling and J. Gallier: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming. 1(3), 267–284, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  20. J. Earley: high-level iterators and a method for automatically designing data structure representation. J. of Computer Languages, 1(4), 1976, 321–342.

    Article  Google Scholar 

  21. A. Fong and J. Ullman: Induction variables in very high-level languages. In Proc. 3rd ACM Symp. on Principles of Programming Languages, 104–112, Jan. 1976.

    Google Scholar 

  22. C. Forgy: RETE, a fast algorithm for the many patterns many objects match problem. Artificial Intelligence, 19(3), 17–37, 1982.

    Article  Google Scholar 

  23. A. Goldberg and R. Paige: Stream processing. In Proceedings of the ACM Symposium on LISP and Functional Programming, ACM, 53–62, 1984.

    Google Scholar 

  24. D. Goyal and R. Paige: The formal reconstruction and improvement of the linear time fragment of Willard’s relational calculus subset. In Algorithmic Languages and Calculi. R. Bird and L. Meertens (Eds.) Chapman & Hall, 382–414, 1997. http://cs.nyu.edu/phd_students/deepak/lrcs.ps.

  25. D. Goyal and R. Paige: A new solution to the hidden copy problem. In Proc. 5th International Static Analysis Symposium. G. Levi (Ed.) LNCS 1503, Springer, 327–348, Sept. 1998. http://cs.nyu.edu/phd_students/deepak/copy.ps.

  26. R. Hindley: The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc., 146, 29–60, 1969.

    Article  MATH  MathSciNet  Google Scholar 

  27. N. Jones, C. Gomard, and P. Sestoft: Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.

    Google Scholar 

  28. J. Keller and R. Paige: Program derivation with verified transformations—a case study. Comm. on Pure and Applied Mathematics, 48 (9–10), 1053–1113, 1996. http://cs.nyu.edu/cs/faculty/paige/papers/ltmjform.ps.

  29. P. Klint: The ASF+SDF meta-environment user’s guide, Version 26. Technical report, Centrum voor Wiskunde en Informatica, 1993.

    Google Scholar 

  30. D. Knuth: The Art of Computer Programming. Vol. 3, Addison-Wesley, 1968–1972.

    Google Scholar 

  31. S. Koenig and R. Paige: A transformational framework for the automatic control of derived data. In Proc. 7th Intl. Conf. on VLDB, 306–318, Sept. 1981.

    Google Scholar 

  32. J. Launchbury and C. K. Holst: Handwriting cogen to avoid problems with static typing. In Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming. C.K.H.R. Heldal and P. Wadler (Eds.) Workshops in Computing, Skye, Scotland, Springer-Verlag, 210–218, 1991.

    Google Scholar 

  33. Y. Liu: Principled strength reduction. In Algorithmic Languages and Calculi. R. Bird and L. Meertens (Eds.) Chapman & Hall, 357–381, 1997.

    Google Scholar 

  34. R. Paige: Formal Differentiation. UMI Research Press, 1981.

    Google Scholar 

  35. R. Paige: Programming with invariants. J IEEE Software, 3(1), 56–69, 1986.

    Article  Google Scholar 

  36. R. Paige: Real-time simulation of a set machine on a RAM. In Computing and Information. N. Janicki and W. Koczkodaj (Eds.). Vol. II of ICCI 89, Canadian Scholars’ Press, Toronto, 69–73, May 1989. http://cs.nyu.edu/cs/faculty/paige/papers/realtime.ps.

  37. R. Paige: Viewing a program transformation system at work. In Programming Language Implementation and Logic, M. Hermenegildo and J. Penjam, (Eds.), LNCS 844, Springer-Verlag, Berlin, 5–24, Sept. 1994.http://cs.nyu.edu/cs/faculty/paige/papers/viewing.ps.

  38. R. Paige and F. Henglein: Mechanical translation of set theoretic problem specifications into efficient RAM code-a case study. Journal of Symbolic Computation, 4(2), 207–232, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  39. R. Paige, R. Tarjan, and R. Bonic: A linear time solution to the single function coarsest partition problem. Theoretical Computer Science, 40(1), 67–84, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  40. R. Paige and Z. Yang: high-level reading and data structure compilation. In Proc. 24 th ACM Symp. on Principles of Programming Languages, 456–469, 1997. http://cs.nyu.edu/phd_students/zheyang/papers/read.ps.

  41. Refine user’s guide version 3.0, 1990.

    Google Scholar 

  42. J. Reif and H. Lewis: Symbolic evaluation and the global value graph. In Proc. 4 th Annual ACM Symp. on Principles of Programming Languages, 104–118, 1997.

    Google Scholar 

  43. T. Reps and T. Teitelbaum: The Synthesizer Generator: A System for Constructing Language-Based Editors. Springer-Verlag, New York, 1989.

    MATH  Google Scholar 

  44. T. Reps, T. Teitelbaum, and A. Demers: Incremental context-dependent analysis for language-based editors. ACM TOPLAS, 5(3), 449–477, 1983.

    Article  Google Scholar 

  45. J. Schwartz: Automatic data structure choice in a language of very high-level. CACM, 18(12), 722–728, 1975.

    MATH  Google Scholar 

  46. J. Schwartz: Optimization of very high-level languages, Parts I, II. J. of Computer Languages, 1(2–3), 161–218, 1975.

    Article  MATH  Google Scholar 

  47. J. Schwartz, Dewar, R., Dubinsky, E., and Schonberg, E.: Programming with Sets: An Introduction to SETL. Springer-Verlag, New York, 1986.

    MATH  Google Scholar 

  48. D. Smith: Kids—a semi-automatic program development system. IEEE Transactions on Software Engineering, 129–136, 1990.

    Google Scholar 

  49. K. Snyder: The SETL2 programming language. Technical Report 490, Courant Insititute, New York University, 1990.

    Google Scholar 

  50. A. Tarski: A lattice-theoretical fixpoint theorem and its application. Pacific J. of Mathematics, 5, 285–309, 1955.

    MATH  MathSciNet  Google Scholar 

  51. J. Ullman: Principles of Database and Knowledge-Base Systems. Computer Science Press, 1988.

    Google Scholar 

  52. E. van der Meulen: Incremental Rewriting. Ph.D. thesis, CWI, Amsterdam, The Netherlands, 1994.

    Google Scholar 

  53. D. E. Willard: Predicate Retrieval Theory. Tech. Report 83-3, SUNY Albany, USA, 1983.

    Google Scholar 

  54. D. E. Willard: Quasi-linear algorithms for processing relational data base expressions. In Proceedings of the 9 th ACM Sigact-Sigmod-Sigart Symposium on Principles of Database Systems, 243–257, 1990.

    Google Scholar 

  55. D. E. Willard: Applications of range query theory to relational data base join and selection operations. J. Computer and System Sci., 52, 157–169, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  56. Z. Yang: Encoding types in ML-like languages. In P. Hudak and C. Queinnec, eds., Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming (Eds.), Baltimore, Maryland, USA, ACM Press, 289–300, 1998.

    Chapter  Google Scholar 

  57. Z. Yang: A native ML implementation of type-directed partial evaluation. In Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE ’98. O. Danvy and P. Dybjer, (Eds.) . Göteborg, Sweden, May 8–9, 1998 , NS-98-1 in BRICS Notes Series, BRICS, Department of Computer Science, University of Aarhus, May 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Courant Institute, New York University, 251 Mercer Street, New York, NY, 10012, USA

    Robert Paige

Authors
  1. Robert Paige
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. BRICS, University of Aarhus, Denmark

    Olivier Danvy

  2. Brandeis University, Waltham, MA, USA

    Harry Mairson

  3. DIKU, University of Copenhagen, Denmark

    Fritz Henglein

  4. DISP, University of Roma ‘Tor Vergata’, Italy

    Alberto Pettorossi

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer

About this chapter

Cite this chapter

Paige, R. (2008). A National Science Foundation Proposal. In: Danvy, O., Mairson, H., Henglein, F., Pettorossi, A. (eds) Automatic Program Development. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-6585-9_2

Download citation

  • DOI: https://doi.org/10.1007/978-1-4020-6585-9_2

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-6584-2

  • Online ISBN: 978-1-4020-6585-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation