Skip to main content
SpringerLink
Log in

Certifying Supercompilation for Martin-Löf’s Type Theory

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2014)

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

  • 506 Accesses

Abstract

The paper describes the design and implementation of a certifying supercompiler TT Lite SC, which takes an input program and produces a residual program and a proof of the fact that the residual program is equivalent to the input one. As far as we can judge from the literature, this is the first implementation of a certifying supercompiler for a non-trivial higher-order functional language. The proofs generated by TT Lite SC can be verified by a type checker which is independent from TT Lite SC and is not based on supercompilation. This is essential in cases where the reliability of results obtained by supercompilation is of fundamental importance. Currently, the proofs can be either verified by the type-checker built into TT Lite, or converted into Agda programs and checked by the Agda system. The main technical contribution is a simple but intricate interplay of supercompilation and type theory.

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    Note that some supercompilers are not semantics-preserving, changing as they do termination properties and/or error handling behavior of programs.

  2. 2.

    Note, however, that the implementation language of the supercompiler does not need to coincide with either the subject language or the proof language.

  3. 3.

    https://github.com/ilya-klyuchnikov/ttlite.

  4. 4.

    This design is similar to that of Coq [14] The numerous and sophisticated Coq “tactics” generate proofs written in Coq’s Core language, which are then verified by a relatively small type checker. Thus, occasional errors in the implementation of tactics do not undermine the reliability of proofs produced by tactics.

  5. 5.

    See [21], Sect. 1.2] describing abstract binding trees.

  6. 6.

    By the way, application is essentially an eliminator for functional values.

  7. 7.

    Recall that application is also a special case of eliminator.

  8. 8.

    Or the graph is declared by the whistle to be “dangerous” (in this case the supercompiler just discards the graph), but this feature is not used by TT Lite SC.

  9. 9.

    In this paper the identity type is only used for constructing proofs of correctness. Thus, for brevity, we do not discuss here driving rules for identity.

  10. 10.

    = “recursive call” of the same eliminator.

References

  1. Sørensen, M.H., Glück, R., Jones, N.D.: A positive supercompiler. J. Funct. Program. 6(6), 811–838 (1996)

    Article  Google Scholar 

  2. Sørensen, M.H., Glück, R.: Introduction to supercompilation. In: Hatcliff, J., Thiemann, P. (eds.) DIKU 1998. LNCS, vol. 1706, pp. 246–270. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(3), 292–325 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  4. Turchin, V.F.: The language Refal: the theory of compilation and metasystem analysis. Technical report 20, Courant Institute of Mathematical Sciences (1980)

    Google Scholar 

  5. Lisitsa, A., Nemytykh, A.: Verification as a parameterized testing. Program. Comput. Softw. 33(1), 14–23 (2007)

    Article  MATH  Google Scholar 

  6. Klimov, A., Klyuchnikov, I., Romanenko, S.: Automatic verification of counter systems via domain-specific multi-result supercompilation. In: [27]

    Google Scholar 

  7. Klyuchnikov, I., Romanenko, S.: Proving the equivalence of higher-order terms by means of supercompilation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 193–205. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Klyuchnikov, I.: Inferring and proving properties of functional programs by means of supercompilation. Ph.D. thesis, Keldysh Institute of Applied Mathematics (2010)

    Google Scholar 

  9. Turchin, V.F.: Supercompilation: techniques and results. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) PSI 1996. LNCS, vol. 1181, pp. 227–248. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  10. Klyuchnikov, I., Romanenko, S.: Towards higher-level supercompilation. In: [28]

    Google Scholar 

  11. Mendel-Gleason, G., Hamilton, G.: Development of the productive forces. In: [27]

    Google Scholar 

  12. Klyuchnikov, I.: Supercompiler HOSC: proof of correctness. Preprint 31, KIAM, Moscow (2010). http://library.keldysh.ru/preprint.asp?id=2010-31

  13. Krustev, D.: A simple supercompiler formally verified in Coq. In: [28], pp. 102–127

    Google Scholar 

  14. Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. Springer, Heidelberg (2010)

    Google Scholar 

  15. The agda wiki (2013). http://wiki.portal.chalmers.se/agda/

  16. Klyuchnikov, I., Romanenko, S.: TT Lite: A Supercompiler for Martin-Löf’s Type Theory. Preprint, KIAM, Moscow (2013). http://library.keldysh.ru//preprint.asp?lg=e&id=2013-73

  17. Martin-Lof, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)

    Google Scholar 

  18. Pardo, A., da Rosa, S.: Program transformation in Martin-Löf’s type theory. In: CADE-12, Workshop on Proof-Search in Type-Theoretic Languages (1994)

    Google Scholar 

  19. Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory. Oxford University Press, Oxford (1990)

    MATH  Google Scholar 

  20. Thompson, S.: Type Theory and Functional Programming. Addison Wesley Longman Publishing Co. Inc., Redwood City (1991)

    MATH  Google Scholar 

  21. Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press, New York (2012)

    Book  Google Scholar 

  22. Löh, A., McBride, C., Swierstra, W.: A tutorial implementation of a dependently typed lambda calculus. Fundamenta Informaticae 21, 1001–1032 (2010)

    Google Scholar 

  23. Klyuchnikov, I.G., Romanenko, S.A.: MRSC: A Toolkit for Building Multi-result Supercompilers. Preprint 77, KIAM (2011). http://library.keldysh.ru/preprint.asp?lg=e&id=2011-77

  24. Jones, N.D.: The essence of program transformation by partial evaluation and driving. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 62–79. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  25. Klyuchnikov, I.: Supercompiler HOSC 1.0: Under the Hood. Preprint 63, KIAM, Moscow (2009). http://library.keldysh.ru/preprint.asp?id=2009-63

  26. Bolingbroke, M., Peyton Jones, S.: Supercompilation by evaluation. In: Proceedings of the Third ACM Haskell Symposium on Haskell, pp. 135–146. ACM (2010)

    Google Scholar 

  27. Klimov, A., Romanenko, S. (eds.) Third International Valentin Turchin Workshop on Metacomputation, Publishing House “University of Pereslavl”, Russia (2012)

    Google Scholar 

  28. Nemytykh, A. (ed.) Second International Valentin Turchin Memorial Workshop on Metacomputation, Publishing House “University of Pereslavl”, Russia (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Keldysh Institute of Applied Mathematics, Moscow, Russia

    Ilya Klyuchnikov & Sergei Romanenko

Authors
  1. Ilya Klyuchnikov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sergei Romanenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ilya Klyuchnikov .

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

  2. A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russia

    Irina Virbitskaite

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klyuchnikov, I., Romanenko, S. (2015). Certifying Supercompilation for Martin-Löf’s Type Theory. In: Voronkov, A., Virbitskaite, I. (eds) Perspectives of System Informatics. PSI 2014. Lecture Notes in Computer Science(), vol 8974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46823-4_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46823-4_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46822-7

  • Online ISBN: 978-3-662-46823-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation