Skip to main content
SpringerLink
Log in

Type-Directed Partial Evaluation

  • Conference paper
Partial Evaluation (DIKU 1998)

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

Included in the following conference series:

Abstract

Type-directed partial evaluation uses a normalization function to achieve partial evaluation. These lecture notes review its background, foundations, practice, and applications. Of specific interest is the modular technique of offline and online type-directed partial evaluation in Standard ML of New Jersey.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction-free normalization proof. In David H. Pitt and David E. Rydeheard, editors, Category Theory and Computer Science, number 953 in LNCS, pages 182–199. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  2. Vincent Balat and Olivier Danvy. Strong normalization by type-directed partial evaluation and run-time code generation. In Xavier Leroy and Atsushi Ohori, editors, Proceedings of the Second International Workshop on Types in Compilation, number 1473 in LNCS, pages 240–252. Springer-Verlag, 1998.

    Google Scholar 

  3. Henk Barendregt. The Lambda Calculus — Its Syntax and Semantics. North-Holland, 1984.

    Google Scholar 

  4. Henk P. Barendregt. Functional Programming and Lambda Calculus, chapter 7, pages 321–364. Volume B of van Leeuwen [38], 1990.

    Google Scholar 

  5. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203–211. IEEE Computer Society Press, 1991.

    Google Scholar 

  6. Lars Birkedal and Morten Welinder. Partial evaluation of Standard ML. Master’s thesis, DIKU, Computer Science Department, University of Copenhagen, August 1993. DIKU Rapport 93/22.

    Google Scholar 

  7. Anders Bondorf and Olivier Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151–195, 1991.

    Article  MATH  Google Scholar 

  8. Anders Bondorf and Jens Palsberg. Generating action compilers by partial evaluation. Journal of Functional Programming, 6(2):269–298, 1996.

    Article  MATH  Google Scholar 

  9. The COMPOSE Project. Effective partial evaluation: Principles and applications. Technical report, IRISA (http://www.irisa.fr), Campus Universitaire de Beaulieu, Rennes, France, January 1996–May 1998. A selection of representative publications.

    Google Scholar 

  10. Charles Consel. New insights into partial evaluation: the Schism experiment. In Harald Ganzinger, editor, Proceedings of the Second European Symposium on Programming, number 300 in LNCS, pages 236–246. Springer-Verlag, 1988.

    Google Scholar 

  11. Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493–501. ACM Press, 1993.

    Google Scholar 

  12. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75–94, 1997.

    Article  MathSciNet  MATH  Google Scholar 

  13. Djordje Čubrić, Peter Dybjer, and Philip Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8:153–192, 1998.

    Article  MathSciNet  MATH  Google Scholar 

  14. Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual A CM Symposium on Principles of Programming Languages, pages 242–257. ACM Press, 1996.

    Google Scholar 

  15. Olivier Danvy. Pragmatics of type-directed partial evaluation. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, Partial Evaluation, number 1110 in LNCS, pages 73–94. Springer-Verlag, 1996. Extended version available as the technical report BRICS RS-96-15.

    Chapter  Google Scholar 

  16. Olivier Danvy. Online type-directed partial evaluation. In Masahiko Sato and Yoshihito Toyama, editors, Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, pages 271–295. World Scientific, 1998. Extended version available as the technical report BRICS RS-97-53.

    Google Scholar 

  17. Olivier Danvy. A simple solution to type specialization. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming, number 1443 in LNCS, pages 908–917. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  18. Olivier Danvy. Type-directed partial evaluation. Lecture Notes BRICS LN-98-3, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1998. Extended version of the present lecture notes.

    MATH  Google Scholar 

  19. Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE’ 98, (Chalmers, Sweden, May 8–9, 1998), number NS-98-1 in BRICS Note Series, Department of Computer Science, University of Aarhus, May 1998.

    Google Scholar 

  20. Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160. ACM Press, 1990.

    Google Scholar 

  21. Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

    Article  MathSciNet  MATH  Google Scholar 

  22. Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. The essence of eta-expansion in partial evaluation. Lisp and Symbolic Computation, 8(3):209–227, 1995.

    Article  Google Scholar 

  23. Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. Eta-expansion does The Trick. ACM Transactions on Programming Languages and Systems, 8(6):730–751, 1996.

    Article  Google Scholar 

  24. Olivier Danvy and Morten Rhiger. Compiling actions by partial evaluation, revisited. Technical Report BRICS RS-98-13, Department of Computer Science, University of Aarhus, Aarhus, Denmark, June 1998.

    Google Scholar 

  25. Olivier Danvy and René Vestergaard. Semantics-based compiling: A case study in type-directed partial evaluation. In Herbert Kuchen and Doaitse Swierstra, editors, Eighth International Symposium on Programming Language Implementation and Logic Programming, number 1140 in LNCS, pages 182–197. Springer-Verlag, 1996. Extended version available as the technical report BRICS-RS-96-13.

    Google Scholar 

  26. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems, chapter 6, pages 243–320. Volume B of van Leeuwen [38], 1990.

    Google Scholar 

  27. Belmina Dzafic. Formalizing program transformations. Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1998.

    Google Scholar 

  28. Andrzej Filinski. Representing monads. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 446–457. ACM Press, 1994.

    Google Scholar 

  29. Andrzej Filinski. From normalization-by-evaluation to type-directed partial evaluation. In Danvy and Dybjer Peter Dybjer, editors. Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE’ 98, (Chalmers, Sweden, May 8–9, 1998), number NS-98-1 in BRICS Note Series, Department of Computer Science, University of Aarhus, May 1998 [19].

    Google Scholar 

  30. Andrzej Filinski. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, LNCS. Springer-Verlag, 1999. To appear. Extended version available as the technical report BRICS RS-99-17.

    Google Scholar 

  31. Mayer Goldberg. Gödelization in the λ-calculus. Technical Report BRICS RS-95-38, Computer Science Department, Aarhus University, Aarhus, Denmark, July 1995.

    Google Scholar 

  32. Mayer Goldberg. Recursive Application Survival in the λ-Calculus. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, May 1996.

    Google Scholar 

  33. Bernd Grobauer. Types for proofs and programs. Progress report, BRICS PhD School, University of Aarhus. Available at http://www.brics.dk/~grobauer, June 1999.

  34. William L. Harrison and Samuel N. Kamin. Modular compilers based on monads transformers. In Purush Iyer and Young il Choo, editors, Proceedings of the IEEE International Conference on Computer Languages, pages 122–131. IEEE Computer Society, 1998.

    Google Scholar 

  35. John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, pages 507–541, 1997. Extended version available as the technical report BRICS RS-96-34.

    Google Scholar 

  36. Simon Helsen and Peter Thiemann. Two flavors of offline partial evaluation. In Jieh Hsiang and Atsushi Ohori, editors, Advances in Computing Science-ASIAN’98, number 1538 in LNCS, pages 188–205. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  37. Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming, 22(3):197–230, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  38. Jan van Leeuwen, managing editor. Handbook of Theoretical Computer Science. The MIT Press, 1990.

    Google Scholar 

  39. Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial evaluation for the lambda calculus. In John Hatcliff, Torben Mogensen and Peter Thiemann, editors, DIKU 1998 International Summerschool on Partial Evaluation, number 1706 in LNCS, pages 203–220. Springer-Verlag, 1999. This volume.

    Google Scholar 

  40. Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice-Hall, 1993.

    Google Scholar 

  41. Jesper Jørgensen. Similix: A self-applicable partial evaluator for Scheme. In John Hatcliff, Torben Mogensen and Peter Thiemann, editors, DIKU 1998 International Summerschool on Partial Evaluation, number 1706 in LNCS, pages 83–107. Springer-Verlag, 1999. This volume.

    Google Scholar 

  42. Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(3):7–105, 1998. Also appears in ACM SIGPLAN Notices 33(9), September 1998.

    Google Scholar 

  43. Julia L. Lawall and Olivier Danvy. Continuation-based partial evaluation. In Carolyn L. Talcott, editor, Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. VII, No. 3. ACM Press, 1994.

    Google Scholar 

  44. Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.

    Google Scholar 

  45. Eugenio Moggi. A categorical account of two-level languages. In Stephen Brookes and Michael Mislove, editors, Proceedings of the 13th Annual Conference on Mathematical Foundations of Programming Semantics, volume 6 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1997.

    Google Scholar 

  46. Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

    Google Scholar 

  47. Jens Palsberg. Eta-redexes in partial evaluation. In John Hatcliff, Torben Mogensen and Peter Thiemann, editors, DIKU 1998 International Summerschool on Partial Evaluation, number 1706 in LNCS, pages 256–366. Springer-Verlag, 1999. This volume.

    Google Scholar 

  48. Jens Palsberg. Correctness of binding-time analysis. Journal of Functional Programming, 3(3):347–363, 1993.

    Article  MathSciNet  Google Scholar 

  49. Morten Rhiger. A study in higher-order programming languages. Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1997.

    Google Scholar 

  50. Morten Rhiger. Deriving a statically typed type-directed partial evaluator. In Olivier Danvy, editor, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 84–88, Technical report BRICS-NS-99-1, University of Aarhus, 1999.

    Google Scholar 

  51. Kristoffer Rose. Type-directed partial evaluation using type classes. In Danvy and Dybjer Peter Dybjer, editors. Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE’ 98, (Chalmers, Sweden, May 8–9, 1998), number NS-98-1 in BRICS Note Series, Department of Computer Science, University of Aarhus, May 1998 [19].

    Google Scholar 

  52. Erik Ruf. Topics in Online Partial Evaluation. PhD thesis, Stanford University, Stanford, California, February 1993. Technical report CSL-TR-93-563.

    Google Scholar 

  53. David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., 1986.

    Google Scholar 

  54. Tim Sheard. A type-directed, on-line, partial evaluator for a polymorphic language. In Charles Consel, editor, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 22–35. ACM Press, 1997.

    Google Scholar 

  55. Guy L. Steele Jr. and Gerald J. Sussman. The art of the interpreter or, the modularity complex (parts zero, one, and two). AI Memo 453, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.

    Google Scholar 

  56. Peter Thiemann. Aspects of the PGG system: Specialization for standard Scheme. In John Hatcliff, Torben Mogensen and Peter Thiemann, editors, DIKU 1998 International Summerschool on Partial Evaluation, number 1706 in LNCS, pages 411–431. Springer-Verlag, 1999. This volume.

    Google Scholar 

  57. Mitchell Wand. Specifying the correctness of binding-time analysis. Journal of Functional Programming, 3(32):365–387, 1993.

    Article  MathSciNet  Google Scholar 

  58. Daniel Weise, Roland Conybeare, Erik Ruf, and Scott Seligman. Automatic online partial evaluation. In John Hughes, editor, Proceedings of the Fifth ACM Conference on Functional Programming and Computer Architecture, number 523 in LNCS, pages 165–191. Springer-Verlag, 1991.

    Google Scholar 

  59. Zhe Yang. Encoding types in ML-like languages. In Paul Hudak and Christian Queinnec, editors, Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming, pages 289–300. ACM Press, 1998. Extended version available as the technical report BRICS RS-98-9.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre of the Danish National Research Foundation, Basic Research in Computer Science, Denmark

    Olivier Danvy

  2. Department of Computer Science, University of Aarhus, Building 540, Ny Munkegade, DK-8000, Aarhus C, Denmark

    Olivier Danvy

Authors
  1. Olivier Danvy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, Manhattan, KS, 66506, USA

    John Hatcliff

  2. DIKU, Københavns Universitet, Universitetsparken 1, DK-2100, København Ø, Denmark

    Torben Æ Mogensen

  3. Institut für Informatik, Universität Freiburg, Universitätsgelände Flugplatz, D-79110, Freiburg i.Br., Germany

    Peter Thiemann

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Danvy, O. (1999). Type-Directed Partial Evaluation. In: Hatcliff, J., Mogensen, T.Æ., Thiemann, P. (eds) Partial Evaluation. DIKU 1998. Lecture Notes in Computer Science, vol 1706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47018-2_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-47018-2_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66710-0

  • Online ISBN: 978-3-540-47018-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation