Lambda the Ultimate

We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, pruning, and an expressive top-level interface. Implementing these additional constructs is well-known in models of backtracking based on streams, but not known to be possible in continuation-based models. We show that all these additional constructs can be generically and monadically realized using a single primitive which we call msplit. We present two implementations of the library: one using success and failure continuations; and the other using control operators for manipulating delimited continuations.

As you can expect from the author list, this is cool stuff. Enjoy!

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi-calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

I guess it's dependent types day around here...

We present a framework called Semantic Streams that allows users to pose declarative queries over semantic interpretations of sensor data. For example, instead of querying raw sensor data, the user can query vehicle speeds; the system decides which sensor data and which operations to use to infer the vehicle speeds. The user can also place constraints on values such as the confidence with which the speed was measured or the amount of energy consumed to measure the speeds. This framework is designed to work in a shared sensor infrastructure, where multiple queries may coexist for extended periods of time, instead of a hand-designed, single purpose sensor network. We propose a semantic service programming model and describe a service description language and a query processor that support the programming model. We demonstrate how this system can be used with a network of video, magnetometer, and infrared break beam sensors deployed in a parking garage.

The declarative framework is based on Prolog and CLP(R) and implemented using SICStus Prolog.

Starlog is a pure-logic programming language designed to overcome some of the problems inherient in traditional approaches to logic programming.

Starlog was designed as an alternative approach to programming in pure logic. Many of the failings of other logic programming languages can be overcome using the bottom-up evaluation technique. Bottom-up evaluation avoids problems associated with cyclic relations, and allows side-effects to be performed without compromising the declarative semantics of a program.

Using Starlog we advocate a data structure free programming style. That is, predicates in Starlog programs do not contain compound terms for their arguments. This greatly simplifies logic programs and their implementations, lowers the learning curve for new programmers, and forces the programmer to think of all program constructs as relations.

I just glanced through this tutorial, but since I know quite a few LtU readers are into proof theory, I thought I'd share the link.

Rys lists several advantages of declarative languages, some of which apply to functional languages in general.

It seems I've become the editor responsible for XML related links around here lately, even though we have on board editors who are much more qualified for this than I am ;-).

This presentation by Raphael Collet provides a nice example of constraint programming, a paradigm we don't discuss often enough.

Experiments from Graham Klyne:

This file is my attempt to better understand the structure and uses
of Description Logic (DL) languages for knowledge reresentation and inference, with the ultimate aim of better understanding the capabilities and limitations of the Semantic Web ontology language OWL, whose design draws much from Description Logic languages.

See also rdfweb-dev post, "Haskell vs. Ada vs. C++ vs. Awk vs. ..., An Experiment in Software Prototyping Productivity" (PS format)

An interesting little Semantic Web-related development reported by Jos De Roo (creator of the Java/C# Euler inference engine). He's got the E Prover (an equational theorem prover for clausal logic), to find a proof for the OWL (Web Ontology Language) test case "inconsistent502" (RDF, variations), which is a Description Logic encoding of one of the classic SAT 3 problems.

A user manual and a technical paper are available.

Reading the paper requires some knowledge of machine learning. The user manual cum tutorial is much more accessible.