Institute for Web Science and Technologies · Universität Koblenz
Institute WeST

Type-safe Programming for the Semantic Web

[go to overview]
Martin Leinberger

Graph-based data formats are flexible in representing data. Inparticular semantic data models, where the schema is part of the data, gainedtraction and commercial success in recent years. Semantic data models are alsothe basis for the Semantic Web—a Web of data governed by open standards inwhich computer programs can freely access the provided data. This thesis isconcerned with the correctness of programs that access semantic data. While theflexibility of semantic data models is one of their biggest strengths, it caneasily lead to programmers accidentally not accounting for unintuitive edgecases. Often, such exceptions surface during program execution as run-timeerrors or unintended side-effects. Depending on the exact condition, a programmay run for a long time before the error occurs and the program crashes.

This thesis defines type systems that can detect and avoid such run-time errorsbased on schema languages available for the Semantic Web. In particular, thisthesis uses the Web Ontology Language (OWL) and its theoretic underpinnings,i.\,e., description logics, as well as the Shapes Constraint Language (SHACL) todefine type systems that provide type-safe data access to semantic data graphs.Providing a safe type system is an established methodology for proving theabsence of run-time errors in programs without requiring execution. Both schemalanguages are based on possible world semantics but differ in the treatment ofincomplete knowledge. While OWL allows for modelling incomplete knowledgethrough an open-world semantics, SHACL relies on a fixed domain and closed-worldsemantics. We provide the formal underpinnings for type systems based on eachof the two schema languages. In particular, we base our notion of types on setsof values which allows us to specify a subtype relation based on subsetsemantics. In case of description logics, subsumption is a routine problem. Forthe type system based on SHACL, we are able to translate it into a descriptionlogic subsumption problem.

10.12.20 - 10:15
via Big Blue Button