Skip to main content
SpringerLink
Log in

Executing Verified Compiler Specification

  • Conference paper
Programming Languages and Systems (APLAS 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2895))

Included in the following conference series:

Abstract

Much work has been done in verifying a compiler specification, both in hand-written and mechanical proofs. However, there is still a gap between a correct compiler specification and a correct compiler implementation. To fill this gap and obtain a correct compiler implementation, we take the approach of generating a compiler from its specification. We verified the correctness of a compiler specification with the theorem prover Isabelle/HOL, and generated a Standard ML code corresponding to the specification with Isabelle’s code generation facility. The generated compiler can be executed with some hand-written codes, and it compiles a small functional programming language into the Java virtual machine with several program transformations.

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. Benton, N., Kennedy, A., Russell, G.: Compiling Standard ML to Java bytecodes. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), vol. 34(1), pp. 129–140 (1999)

    Google Scholar 

  2. Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 24–40. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Bothner, P.: Kawa—compiling dynamic languages to the Java VM. In: Proceedings of the USENIX, Technical Conference, FREENIX Track, New Orleans, LA, USENIX Association (1998)

    Google Scholar 

  4. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, London (1988)

    MATH  Google Scholar 

  5. Curzon, P.: A verified Vista implementation final report. Technical Report 311, University of Cambridge Computer Laboratory (1993)

    Google Scholar 

  6. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  7. Hannan, J.: A type system for closure conversion. In: Proceedings of the Workshop on Types for Program Analysis, pp. 48–62 (1995)

    Google Scholar 

  8. Klein, G., Nipkow, T.: Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience 13, 1133–1151 (2001)

    Article  MATH  Google Scholar 

  9. Klein, G., Nipkow, T.: Verified bytecode verifiers. Theoretical Computer Science 298, 583–626 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  10. Meyer, J.: Jasmin home page, http://mrl.nyu.edu/~meyer/jasmin/

  11. Minamide, Y., Morrisett, J.G., Harper, R.: Typed closure conversion. In: Proceedings of Symposium on Principles of Programming Languages, pp. 271– 283 (1996)

    Google Scholar 

  12. Moore, J.S.: A mechanically verified language implementation. Technical Report 30, Computational Logic Inc. (1988)

    Google Scholar 

  13. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL : A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  14. Oliva, D.P., Ramsdell, J.D., Wand, M.: The VLISP verified PreScheme compiler. Lisp and Symbolic Computation 8(1/2), 111–182 (1995)

    Article  Google Scholar 

  15. Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA (September 1999)

    Google Scholar 

  16. Stepney, S.: High Integrity Compilation: a case study. Prentice-Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  17. Stringer-Calvert, D.W.: Mechanical Verification of Compiler Correctness. PhD thesis, Department of Computer Science, University of York (March 1998)

    Google Scholar 

  18. Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Proceedings of International Conference on Theorem Proving in Higher Order Logics, pp. 167–184 (1999)

    Google Scholar 

  19. Young, W.D.: A verified code generator for a subset of Gypsy. Technical Report 33, Computational Logic Inc. (1988)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Doctoral Program in Engineering, University of Tsukuba,  

    Koji Okuma

  2. Institute of Information Sciences and Electronics, University of Tsukuba,  

    Yasuhiko Minamide

Authors
  1. Koji Okuma
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yasuhiko Minamide
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Information Science, Japan Advanced Institute of Science and Technology, Tatsunokuchi, Ishikawa, Japan

    Atsushi Ohori

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Okuma, K., Minamide, Y. (2003). Executing Verified Compiler Specification. In: Ohori, A. (eds) Programming Languages and Systems. APLAS 2003. Lecture Notes in Computer Science, vol 2895. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40018-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-40018-9_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20536-4

  • Online ISBN: 978-3-540-40018-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation