Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 1996: Theorem Proving in Higher Order Logics pp 347–361Cite as

Verification of compiler correctness for the WAM

  • Conference paper
  • First Online:

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

Abstract

Relying on an derivation of the Warren Abstract Machine (WAM) by stepwise refinement of Prolog models by Börger and Rosenzweig we present a formalization of an operational semantics for Prolog. Then we develop four refinement steps towards the Warren Abstract Machine (WAM). The correctness and completeness proofs for each step have been elaborated with the theorem prover Isabelle using the logic HOL.

Research supported by DFG grant Br 887/4-3, Deduktive Programmentwicklung

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Hassan Aït-Kaci. Warren's Abstract Machine, A Tutorial Reconstruction. MIT Press, Cambridge, Massachusetts, 1991.

    Google Scholar 

  2. Krzysztof R. Apt. Logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 10, pages 495–574. Elsevier Science Publishers B.V., 1990.

    Google Scholar 

  3. Patrice Boizumault. The Implementation of Prolog. Princeton Series in Computer Science. Princeton University Press, Princeton, New Jersey, 1993.

    Google Scholar 

  4. E. Börger and D. Rosenzweig. The WAM-Definition and Compiler Correctness. In C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications. Elsevier, 1994.

    Google Scholar 

  5. Saumya K. Debray and Prateek Mishra. Denotational and Operational Semantics for Prolog. J. Logic Programming, (5):61–91, 1988.

    Google Scholar 

  6. Yuri Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.

    Google Scholar 

  7. J. W. Lloyd. Foundations of Logic Programming. Springer, 1987.

    Google Scholar 

  8. L.C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.

    Google Scholar 

  9. David M. Russinoff. A Verified Prolog Compiler for the Warren Abstract Machine. J. Logic Programming, (13):367–412, 1992.

    Google Scholar 

  10. G. Schellhorn. Von PROLOG zur WAM-Compilerverifikation mit KIV. Talk at the annual meeting of the GI section “Logic in Computer Science”, Karlsruhe, Juni 1995.

    Google Scholar 

  11. D. H. Warren. An Abstract Prolog Instruction Set. Technical Report 309, SRI International, 1083.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität München, 80290, München, Germany

    Cornelia Pusch

Authors
  1. Cornelia Pusch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gerhard Goos Juris Hartmanis Jan van Leeuwen Joakim von Wright Jim Grundy John Harrison

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pusch, C. (1996). Verification of compiler correctness for the WAM. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1996. Lecture Notes in Computer Science, vol 1125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0105415

Download citation

  • DOI: https://doi.org/10.1007/BFb0105415

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61587-3

  • Online ISBN: 978-3-540-70641-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation