Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 1995: Higher Order Logic Theorem Proving and Its Applications pp 170–185Cite as

Interfacing HOL90 with a functional database query language

  • Conference paper
  • First Online:

  • 181 Accesses

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

Abstract

We describe a functional database language OR-SML for handling disjunctive information in database queries, its implementation in Standard ML [10], and its interface to HOL90. The core language has the power of the nested relational algebra, and it is augmented with or-sets which are used to deal with disjunctive information. Sets, or-sets and tuples can be freely combined to create objects, which gives the language a greater flexibility. We give an example of queries over the “database” of HOL90 theories which require disjunctive information and show how to use the language to answer these queries. Since the system is running on top of Standard ML and all database objects are values in the latter, the system benefits from combining a sophisticated query language with the full power of a programming language. The language has been implemented as an HOL90-loadable library of modules in Standard ML.

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. V. Breazu-Tannen, P. Buneman, and S. Naqvi. Structural recursion as a query language. In Proc. of 3rd Int. Workshop on Database Programming Languages, pages 9–19, Naphlion, Greece, August 1991.

    Google Scholar 

  2. V. Breazu-Tannen, P. Buneman, and L. Wong. Naturally embedded query languages. In LNCS 646: Proc. ICDT, Berlin, Germany, October, 1992, pages 140–154. Springer-Verlag, October 92.

    Google Scholar 

  3. V. Breazu-Tannen and R. Subrahmanyam. Logical and computational aspects of programming with sets/bags/lists. In LNCS 510: Proc. of ICALP-1991, Springer Verlag, 1991, pages 60–75.

    Google Scholar 

  4. L. Colby, A recursive algebra for nested relations, Inform. Systems 15 (1990), 567–582.

    Google Scholar 

  5. S. Grumbach, T. Milo, Towards tractable algebras for bags, Proc. 12th Symposium on Principles of Database Systems, Washington DC, 1993, pages 49–58.

    Google Scholar 

  6. E. Gunter and L. Libkin, OR-SML: A functional database programming language for disjunctive information and its applications, In: D. Karagiannis ed., Proc. 5th Internat. Conf. on Database and Expert Systems Applications (DEXA '94), Athens, Greece, September 1994. Springer-Verlag LNCS vol. 856, 1994, pp. 641–650.

    Google Scholar 

  7. L. Libkin. Normalizing incomplete databases. In Proceedings of the 14th Symp. on Principles of Database Systems, San Jose CA, 1995, pages 219–230.

    Google Scholar 

  8. L. Libkin and L. Wong, Semantic representations and query languages for or-sets, Proceedings of the 12th Symp. on Principles of Database Systems, Washington DC, 1993, pages 37–48.

    Google Scholar 

  9. L. Libkin and L. Wong, Some properties of query languages for bags, In Proceedings of the 4th International Workshop on Database Programming Languages, September 1993, Springer Verlag, 1994, pages 97–114.

    Google Scholar 

  10. R. Milner, M. Tofte, R. Harper, “The Definition of Standard ML”, The MIT Press, Cambridge, Mass, 1990.

    Google Scholar 

  11. A. Ohori, V. Breazu-Tannen and P. Buneman, Database programming in Machiavelli: a polymorphic language with static type inference, In SIGMOD 89, pages 46–57.

    Google Scholar 

  12. H.-J. Schek and M. Scholl, The relational model with relation-valued attributes, Inform. Systems 11 (1986), 137–147.

    Google Scholar 

  13. S.J. Thomas and P. Fischer, Nested relational structures, in P. Kanellakis ed., Advances in Computing Research: The Theory of Databases, pages 269–307, JAI Press, 1986.

    Google Scholar 

  14. P.W. Trinder, Comprehension: A query notation for DBPLs, In Proc. 3rd Int. Workshop on Database Progr. Languages, 1991, pages 49–62, Morgan Kaufmann.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AT&T Bell Laboratories, Rm.#2A-432 600 Mountain Ave., 07974, Murray Hill, N.J., USA

    Elsa L. Gunter

  2. AT&T Bell Laboratories, Rm.#2A-422, USA

    Leonid Libkin

Authors
  1. Elsa L. Gunter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Leonid Libkin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

E. Thomas Schubert Philip J. Windley James Alves-Foss

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gunter, E.L., Libkin, L. (1995). Interfacing HOL90 with a functional database query language. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_64

Download citation

  • DOI: https://doi.org/10.1007/3-540-60275-5_64

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation