Skip to main content
SpringerLink
Log in
Book cover

HOL Users' Group Workshop

HUG 1993: Higher Order Logic Theorem Proving and Its Applications pp 295–309Cite as

Domain theory in HOL

  • Conference paper
  • First Online:

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

Abstract

In this paper we present a formalization of domain theory in HOL. The notions of complete partial order, continuous function and inclusive predicate are introduced as semantic constants in HOL and fixed point induction is a derived theorem, just as we can derive other techniques for recursion. We provide tools which prove certain terms are cpos, continuous functions or inclusive predicates, automatically.

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. H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.

    Google Scholar 

  2. A.J. Camilleri, ‘Mechanizing CSP Trace Theory in Higher Order Logic'. IEEE Transactions on Software Engineering, Vol. 16, No. 9, September 1990.

    Google Scholar 

  3. M.J.C. Gordon, R. Milner and C.P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation. Springer-Verlag, LNCS 78, 1979.

    Google Scholar 

  4. B. Jacobs and T. Melham, ‘Translating Dependent Type Theory into Higher Order Logic'. In the Proceedings of the International Conference on Typed Lambda Calculi and Applications, Utrecht, 16–18 March 1993. Springer-Verlag, LNCS 664, 1993.

    Google Scholar 

  5. L.C. Paulson, Logic and Computation. Cambridge Tracts in Theoretical Computing 2, Cambridge University Press, 1987.

    Google Scholar 

  6. K.D. Petersen, ‘Graph Model of LAMBDA in Higher Order Logic'. In the Proceedings of the 1993 International Meeting on Higher Order Logic Theorem Proving and Its Applications, Vancouver Canada, 11–13 August 1993 (Springer-Verlag, LNCS Series).

    Google Scholar 

  7. D.A. Schmidt, Denotational Semantics. Allyn and Bacon, 1986.

    Google Scholar 

  8. D. Scott, ‘Data Types as Lattices'. SIAM J. Comput., Vol. 5, No. 3, September 1976.

    Google Scholar 

  9. J.E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, 1977.

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Aarhus University, DK-8000, Aarhus C, Denmark

    Sten Agerholm

Authors
  1. Sten Agerholm
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jeffrey J. Joyce Carl-Johan H. Seger

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Agerholm, S. (1994). Domain theory in HOL. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_143

Download citation

  • DOI: https://doi.org/10.1007/3-540-57826-9_143

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57826-0

  • Online ISBN: 978-3-540-48346-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation