Skip to main content
SpringerLink
Log in

A Note on Specialization of Interpreters

  • Conference paper
Computer Science – Theory and Applications (CSR 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4649))

Included in the following conference series:

Abstract

Given a program with two arguments p(x,y). Let the first argument x0 be fixed. The aim of program specialization with respect to the known x0 is to construct an optimized program P x 0(y) such that P x 0(y) = P(x0,y). Specialization of interpreters with respect to programs is well known problem. In this paper we argue that specialization of interpreters with respect to data may be seen as program verification.

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. Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bundy, A.: The Automation of Proof by Mathematical Induction. Handbook of Automated Reasoning, 845–911 (2001)

    Google Scholar 

  3. Cheng, K.T., Krishnakumar, A.S.: Automatic Generation of Functional Vectros Using the Extended Finite State Machine Model. ACM Transactions on Design Automation of Electronic Systems 1(1), 57–79 (1996)

    Article  Google Scholar 

  4. Delzanno, G.: Automatic Verification of Parameterized Cache Coherence Protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–68. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Delzanno, G.: Automatic Verification of Cache Coherence Protocols via Infinite-state Constraint-based Model Checking, http://www.disi.unige.it/person/DelzannoG/protocol.html

  6. Delzanno, G.: Verification of Consistency Protocols via Infinite-state Symbolic Model Checking, A Case Study. In: Proc. of FORTE/PSTV, pp. 171–188 (2000)

    Google Scholar 

  7. Delzanno, G., Bultan, T.: Constraint-Based Verification of Client-Server Protocols. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 286–301. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Futamura, Y.: Partial Evaluation of Computation Process — An Approach to a Compiler-Compiler. Systems. Computers. Controls 2(5), 45–50 (1971)

    Google Scholar 

  9. Futamura, Y., Nogi, K., Takano, A.: Essence of generalized partial computation. Theoretical Computer Science 90, 61–79 (1991)

    Article  MATH  Google Scholar 

  10. Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2(7), 326–336 (1952)

    Article  MATH  MathSciNet  Google Scholar 

  11. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall International, Englewood Cliffs (1993)

    MATH  Google Scholar 

  12. Jones, N.D.: What not to do when writing an interpreter for specialization. In: Danvy, O., Thiemann, P., Glück, R. (eds.) Partial Evaluation. LNCS, vol. 1110, pp. 216–237. Springer, Heidelberg (1996)

    Google Scholar 

  13. Korlyukov, A.V.: User manual on the Supercompiler SCP4 (in Russian) (1999), http://www.refal.net/supercom.htm

  14. Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture. Trans. Amer. Math. Society 95, 210–225 (1960)

    Article  MATH  MathSciNet  Google Scholar 

  15. Leuschel, M.: Homeomorphic Embedding for Online Termination. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 199–218. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Lisitsa, A., Nemytykh, A.P.: Verification of parameterized systems using supercompilation. A case study. In: Hofmann, M., Loidl, H.W. (eds.) APPSEM 2005. Proc. of the Third Workshop on Applied Semantics, Fraunchiemsee, Germany. Ludwig Maximillians Universitat Munchen (2005), Accessible via: ftp://www.botik.ru/pub/local/scp/refal5/appsem_verification2005.ps

  17. Lisitsa, A.P., Nemytykh, A.P.: Work on errors (in Russian). In: Program Systems: Theory and Applications (Programmnye systemy: teoriya i prilozheniya) Fizmatlit, Moscow, vol. 1, pp. 195–232 (2006), Accessible via: ftp://www.botik.ru/pub/local/scp/refal5/psta_errors2006.pdf

  18. Lisitsa, A.P., Nemytykh, A.P.: Verification as a Parameterized Testing (Experiments with the SCP4 Supercompiler). Programmirovanie. 1 (2007) (In Russian). English translation in J. Programming and Computer Software, 33(1), 14–23 (2007)

    Google Scholar 

  19. Lisitsa, A.P., Nemytykh, A.P.: Reachability Analysis in Verification via Supercompilation. Accepted by the Workshop on Reachability Problems - RP07

    Google Scholar 

  20. Mogensen, T.: Evolution of Partial Evaluators: Removing Inherited Limits. In: Danvy, O., Thiemann, P., Glück, R. (eds.) Partial Evaluation. LNCS, vol. 1110, pp. 303–321. Springer, Heidelberg (1996)

    Google Scholar 

  21. Nemytykh, A.P.: A Note on Elimination of Simplest Recursions. In: Proc. of the ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 138–146. ACM Press, New York (2002)

    Google Scholar 

  22. Nemytykh, A.P.: The Supercompiler SCP4: General Structure (extended abstract). In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 162–170. Springer, Heidelberg (2004)

    Google Scholar 

  23. Nemytykh, A.P.: Playing on REFAL. In: Proc. of the International Workshop on Program Understanding, A.P. Ershov Institute of Informatics Systems, Syberian Branch of Russian Academy of Sciences, pp. 29–39 (2003), Accessible via: ftp://www.botik.ru/pub/local/scp/refal5/nemytykh_PU03.ps.gz

  24. Nemytykh, A.P.: The Supercompiler SCP4: General Structure. Moscow, URSS (A book in Russian, to appear)

    Google Scholar 

  25. Nemytykh, A.P., Turchin, V.F.: The Supercompiler SCP4: sources, on-line demonstration (2000), http://www.botik.ru/pub/local/scp/refal5/

  26. Pettorossi, A., Proietti, M.: Transformation of logic programs: Foundations and techniques. J. of Logic Programming 19,20, 261–320 (1994)

    Article  MathSciNet  Google Scholar 

  27. Turchin, V.F.: The use of metasystem transition in theorem proving and program optimization. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 645–657. Springer, Heidelberg (1980)

    Google Scholar 

  28. Turchin, V.F.: The language Refal - The Theory of Compilation and Metasystem Analysis. Courant Computer Science Report, New York University, vol. 20 (February 1980)

    Google Scholar 

  29. Turchin, V.F.: The concept of a supercompiler. ACM Transactions on Programming Languages and Systems 8, 292–325 (1986)

    Article  MATH  Google Scholar 

  30. Turchin, V.F.: Refal-5, Programming Guide and Reference Manual. New England Publishing Co. Holyoke, Massachusetts (1989), (electronic version: http://www.botik.ru/pub/local/scp/refal5/,2000 )

  31. Turchin, V.F., Turchin, D.V., Konyshev, A.P., Nemytykh, A.P.: Refal-5: sources, executable modules (2000), http://www.botik.ru/pub/local/scp/refal5/

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Liverpool,  

    Alexei Lisitsa

  2. Program Systems Institute of Russian Academy of Sciences,  

    Andrei P. Nemytykh

Authors
  1. Alexei Lisitsa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei P. Nemytykh
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Volker Diekert Mikhail V. Volkov Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lisitsa, A., Nemytykh, A.P. (2007). A Note on Specialization of Interpreters. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds) Computer Science – Theory and Applications. CSR 2007. Lecture Notes in Computer Science, vol 4649. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74510-5_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74510-5_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74509-9

  • Online ISBN: 978-3-540-74510-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation