Logic/Declarative

Behaviour: Using CSS selectors to apply Javascript functionality

An amusing library that lets you use CSS selectors to specify elements to add javascript events to.

The terms pattern matching, and declartive programming come mind.

You can also think about it as an embedded DSL.

I came across Behaviour via this simple example which shows the style of programming the library leads to.

Backtracking, Interleaving, and Terminating Monad Transformers

Backtracking, Interleaving, and Terminating Monad Transformers. Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman and Amr Sabry.

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!

A type discipline for authorization policies

A type discipline for authorization policies. Cedric Fournet; Andrew D. Gordon; Sergio Maffeis

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...

Semantic Streams: a Framework for Declarative Queries and Automatic Data Interpretation

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

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.

A Tutorial on Proof Theoretic Foundations of Logic Programming

A Tutorial on Proof Theoretic Foundations of Logic Programming. Paola Bruscoli and Alessio Guglielmi. ICLP'03.

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.

XQuery and XSLT as declarative languages

More from Michael Rys.

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 ;-).

Playing the Minesweeper with Constraints (MOZ 2004)

Peter linked to the MOZ 2004 papers earlier.

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

Description Logics in Literate Haskell

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)

SAT 3 Proof with E Prover via OWL

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.

XML feed