Interfacing HOL90 with a functional database query language

Elsa L. Gunter, Leonid Libkin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 HOLg0 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-1oadable library of modules in Standard ML.

Original languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 8th International Workshop, Proceedings
EditorsE. Thomas Schubert, Phillip J. Windley, James Alves-Foss
Number of pages15
ISBN (Print)3540602755, 9783540602750
StatePublished - Jan 1 1995
Externally publishedYes
Event8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995 - Aspen Grove, United States
Duration: Sep 11 1995Sep 14 1995

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995
Country/TerritoryUnited States
CityAspen Grove

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Interfacing HOL90 with a functional database query language'. Together they form a unique fingerprint.

Cite this