Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 1996: Foundations of Software Technology and Theoretical Computer Science pp 180–192Cite as

Winskel is (almost) right

Towards a mechanized semantics textbook

  • Conference paper
  • First Online:

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

Abstract

We present a formalization of the first 100 pages of Winskel's The Formal Semantics of Programming Languages in the theorem prover Isabelle/HOL: 2 operational, 2 denotational, 1 axiomatic semantics, a verification condition generator, and the necessary soundness, completeness and equivalence proofs, all for a simple imperative language.

Research supported by DFG Schwerpunktprogramm Deduktion.

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. Y. Bertot and R. Fraer. Reasoning with executable specifications. In TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lect. Notes in Comp. Sci., pages 531–545. Springer-Verlag, 1995.

    Google Scholar 

  2. M. Gordon. Programming Language Theory and its Implementation. Prentice-Hall, 1988.

    Google Scholar 

  3. M. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989.

    Google Scholar 

  4. M. Gordon and T. Melham. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.

    Google Scholar 

  5. P. V. Homeier and D. F. Martin. Trustworthy tools for trustworthy programs: A verified verification condition generator. In T. Melham and J. Camilleri, editors, Higher Order Logic Theorem Proving and its Applications, volume 859 of Lect. Notes in Comp. Sci., pages 269–284. Springer-Verlag, 1994.

    Google Scholar 

  6. H. Lötzbeyer and R. Sandner. Proof of the equivalence of the operational and denotational semantics of IMP in Isabelle/ZF. Project report, Institut für Informatik, TU München, 1994.

    Google Scholar 

  7. L. C. Paulson. Logic and Computation. Cambridge University Press, 1987.

    Google Scholar 

  8. L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.

    Google Scholar 

  9. L. C. Paulson. Generic automatic proof tools. Technical Report 396, University of Cambridge, Computer Laboratory, 1996.

    Google Scholar 

  10. F. Regensburger. HOLCF: Eine konservative Erweiterung von HOL um LCF. PhD thesis, Technische UniversitÄt München, 1994.

    Google Scholar 

  11. F. Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lect. Notes in Comp. Sci., pages 293–307. Springer-Verlag, 1995.

    Google Scholar 

  12. L. van Benthem Jutting. Checking Landau's “Grundlagen” in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977.

    Google Scholar 

  13. G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, TU München, 80290, München, Germany

    Tobias Nipkow

Authors
  1. Tobias Nipkow
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

V. Chandru V. Vinay

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nipkow, T. (1996). Winskel is (almost) right. In: Chandru, V., Vinay, V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1996. Lecture Notes in Computer Science, vol 1180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62034-6_48

Download citation

  • DOI: https://doi.org/10.1007/3-540-62034-6_48

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62034-1

  • Online ISBN: 978-3-540-49631-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation