Type Checking Semantically Lifted Programs via Query Containment under Entailment Regimes

Abstract

Semantically lifted programs integrate declarative ontologybased knowledge modelling into imperative programming. In this approach, each state of a program is mapped into an OWL knowledge base (KB) and enriched with user-dfined knowledge; the resulting KB can be accessed from the program using standard SemanticWeb queries. The result of a query, however, should conform the type system of the program. We present a technique for checking type conformance statically, which is based on query containment over OWL KBs. We then discuss an approximation method for type checking, which exploits concept subsumption rather than containment and hence allows for an effcient implementation using existing tools. Finally, we describe our implementation of semantically lifted programs with static type checking in language SMOL.