WLP 2016 Talk Schedule and Slides

Monday September 12

• 14:00 - 15:00 WLP Session: Deductive Databases (Chair: Stefan Brass)
  Falco Nogatz and Dietmar Seipel.
  GraphQL as a Query Language for Deductive Databases - An Implementation in SWI-Prolog with DCGs (slides)
  Abstract:
  The methods to access large relational databases in a distributed system are well established: the relational query language SQL often serves as a low-level language for data access and manipulation, and in addition several endpoints are exposed by public interfaces using for example REST. Similarly to REST, GraphQL is the query protocol of an application layer developed by Facebook. It provides a unified interface between the client and the server for data fetching and manipulation. Using GraphQL's type system, it is possible to specify data handling of various sources and combine, e.g., relational with NoSQL databases. In contrast to REST, GraphQL provides a single endpoint and supports flexible queries over linked data. This makes GraphQL a perfect fit as an interface for deductive databases. In this paper, we give an introduction of GraphQL and a comparison to REST. Using language features recently added to SWI-Prolog 7, we have developed the Prolog library GraphQL.pl, which implements the GraphQL type system and query syntax as a domain-specific language with the help of DCGs. Using our library, the type system created for a deductive database can be validated, while the query system provides a unified interface for data access and introspection.
  Stefan Brass and Heike Stephan.
  Experiences with Some Benchmarks for Deductive Databases and Implementations of Bottom-Up Evaluation
  Abstract:
  OpenRuleBench [LFWK09] is a large benchmark suite for rule engines, which includes deductive databases. We previously proposed a translation of Datalog to C++ based on a method that "pushes" derived tuples immediately to places where they are used. In this paper, we report preformance results of various implementation variants of this method compared to XSB, YAP and DLV. We study only a fraction of the OpenRuleBench problems, but we give a quite detailed analysis of each such task and the factors which influence performance. The results not only show the potential of our method and implementation approach, but could be valuable for anybody implementing systems which should be able to execute tasks of the discussed types.
• 15:30 - 16:45 Mitgliederversammlung
  der Gesellschaft für Logische Programmierung e.V. (GLP)
  incl. Wahl der Sprecher der GI-Fachgruppe Deklarative Sprachen
• 18:30 WLP/WFLP reception (celebration of 30th WLP)
Dinner Talk by Ulrich Geske, Univ. Potsdam.
WLP^meta
oder WLP: woher, wohin - und warum?
Abstract:
Kein Beitrag zum WLP, sondern über den WLP: Zeitpunkte, Orte, Namen, Zahlen, Themen, Sammlungen, Statistiken und auch Fragen.

(F)(C)LP -> Deklarative Programmierung?

Werden Ansprüche erfüllt, sind sie erfüllbar? Sind sich inzwischen alle einig (Uniting-Call 2008)? Wie ist die Ausstrahlung von (F)(C)LP? Warum deklarativ programmieren? Welches Interesse besteht an den Arbeiten im WLP? Wie wird es geweckt? Was wäre anzugehen, um einen 130.WLP möglich zu machen?

Antworten muss die Community liefern.

Tuesday September 13

• 09:00 - 10:00 WLP Session: Verification (Chair: Dietmar Seipel)
  Sebastian Krings and Michael Leuschel.
  Constraint Logic Programming over Infinite Domains with an Application to Proof (slides)
  Abstract:
  We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration as a last resort. An important aspect is detecting when enumeration was complete and if this has an impact on the soundness of the result. We present a technique which guarantees soundness in the following way: if the constraint solver finds a solution it is guaranteed to be correct; if the constraint solver fails to find a solution it can either return the result "definitely false'' in case it knows enumeration was exhaustive, or "unknown'' in case it was aborted. The technique can deal with nested universal and existential quantifiers. It can easily be extended to set comprehensions and other operators introducing new quantified variables. We show applications in data validation and proof.
  Frank Flederer, Ludwig Ostermayer, Dietmar Seipel and Sergio Montenegro.
  Source Code Verification for Embedded Systems using Prolog
  Abstract:
  System relevant embedded software needs to be reliable and therefore well tested, especially for aerospace systems. A common technique to verify programs is the analysis of their abstract syntax tree (AST). Tree-like structures can be elegantly analyzed with the logic programming language Prolog. Moreover, Prolog offers further advantages for a thorough analysis: On the one hand, it natively provides versatile options to efficiently process tree- or graph-like data structures. On the other hand, Prolog's non-determinism and backtracking allows to test for different variations of the program flow without big effort. A rule-based approach with Prolog enables a concise and declarative characterization of the verification goals in a concise and declarative way. In this paper, we describe our approach to verify the source code of a flash file system with the help of Prolog. The flash file system is written in C++ and has been developed particularly for use within satellites. We transform a given abstract syntax tree of C++ source code into Prolog facts and derive a call graph and the execution sequence, which then are further tested against the verification goals. The different program flow branching due to control structures is derived by backtracking as subtrees of the original AST. Finally, these subtrees are verified in Prolog. We illustrate our approach with a case study, where we search for incorrect applications of semaphores in a flash file system for satellites. We rely on computation tree logic (CTL) and have designed an embedded domain specific language (DSL) in Prolog to express the verification goals.
• 10:20 - 11:20 WFLP Invited Talk:
  Anthony Anjorin.
  Declarative Model Transformations with Triple Graph Grammars
• 11:40 WFLP Sessions
• 16:00 WLP/WFLP excursion and dinner