Advertisement

Isomorphisms — A Link Between the Shallow and the Deep

  • Thomas Santen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1690)

Abstract

We present a theory of isomorphisms between typed sets in Isabelle/HOL. Those isomorphisms can serve to link a shallow embedding with a theory that defines certain concepts directly in HOL. Thus, it becomes possible to use the advantage of a shallow embedding that it allows for efficient proofs about concrete terms of the embedded formalism with the advantage of a deeper theory that establishes general abstract propositions about the key concepts of the embedded formalism as theorems in HOL.

Keywords

Theorem Prove High Order Logic Abstraction Function Concrete Classis Proof Script 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    J. Bowen and M. Gordon. A shallow embedding of Z in HOL. Information and Software Technology, 37(5–6):269–276, 1995.CrossRefGoogle Scholar
  2. [2]
    L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.CrossRefGoogle Scholar
  3. [3]
    M. Gordon. Set theory, higher order logic or both? In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, LNCS 1125, pages 191–201. Springer-Verlag, 1996.CrossRefGoogle Scholar
  4. [4]
    M. J. C. Gordon and T. M. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
  5. [5]
    U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In C. Hankin, editor, Programming Languages and Systems-7th European Symposium on Programming, ESOP’98, LNCS 1381, pages 105–121. Springer-Verlag, 1998.CrossRefGoogle Scholar
  6. [6]
    C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271–281, 1972.CrossRefMATHGoogle Scholar
  7. [7]
    Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher-Order Logics, LNCS 1125, pages 283–298. Springer-Verlag, 1996.CrossRefGoogle Scholar
  8. [8]
    L. Lamport and L. C. Paulson. Should your specification language be typed? http://www.cl.cam.ac.uk/users/lcp/papers/lamport-paulson-types.ps.gz, 1997.
  9. [9]
    B. Meyer. Reusable Software. Prentice Hall, 1994.Google Scholar
  10. [10]
    O. Müller. I/O automata and beyond: temporal logic and abstraction in Isabelle. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, LNCS 1479, pages 331–348. Springer-Verlag, 1998.CrossRefGoogle Scholar
  11. [11]
    O. Müller and K. Slind. Treating partiality in a logic of total functions. The Computer Journal, 40(10):640–651, 1997.CrossRefGoogle Scholar
  12. [12]
    W. Naraschewski and M. Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics — 11th International Conference, TPHOLs’98, LNCS 1479, pages 349–366. Springer-Verlag, 1998.CrossRefGoogle Scholar
  13. [13]
    T. Nipkow. More Church/Rosser proofs (in Isabelle/HOL). In Automated Deduction — CADE 14, LNCS 1104, pages 733–747. Springer-Verlag, 1996.Google Scholar
  14. [14]
    S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Laboratory, 1993.Google Scholar
  15. [15]
    L. C. Paulson. Isabelle–A Generic Theorem Prover. LNCS 828. Springer-Verlag, 1994.MATHGoogle Scholar
  16. [16]
    T. Santen. A theory of structured model-based specifications in Isabelle/HOL. In E. L. Gunter and A. Felty, editors, Proc. International Conference on Theorem Proving in Higher Order Logics, LNCS 1275, pages 243–258. Springer-Verlag, 1997.CrossRefGoogle Scholar
  17. [17]
    T. Santen. On the semantic relation of Z and HOL. In J. Bowen and A. Fett, editors, ZUM’98: The Z Formal Specification Notation, LNCS 1493, pages 96–115. Springer-Verlag, 1998.Google Scholar
  18. [18]
    T. Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. PhDthesis, Fachbereich Informatik, Technische Universität Berlin, Germany, 1999. forthcoming.Google Scholar
  19. [19]
    J. M. Spivey. The Z Notation — A Reference Manual. Prentice Hall, 2nd edition, 1992.Google Scholar
  20. [20]
    H. Tej and B. Wolff. A corrected failure-divergence model for CSP in Isabelle/HOL. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME’97: Industrial Applications and Strengthened Foundations of Formal Methods, LNCS 1313, pages 318–337. Springer-Verlag, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Thomas Santen
    • 1
  1. 1.Softwaretechnik, FR 5-6 Fachbereich InformatikTechnische Universität BerlinBerlinGermany

Personalised recommendations