Abstract interpretation for constraint handling rules

Abstract interpretation for constraint handling rules. Tom Schrijvers, Peter J. Stuckey, Gregory J. Duck. PPDP’05

Program analysis is essential for the optimized compilation of Constraint Handling Rules (CHRs) as well as the inference of behavioral properties such as confluence and termination. Up to now all program analyses for CHRs have been developed in an ad hoc fashion.In this work we bring the general program analysis methodology of abstract interpretation to CHRs: we formulate an abstract interpretation framework over the call-based operational semantics of CHRs. The abstract interpretation framework is non-obvious since it needs to handle the highly non-deterministic execution of CHRs. The use of the framework is illustrated with two instantiations: the CHR-specific late storage analysis and the more generally known groundness analysis. In addition, we discuss optimizations based on these analyses and present experimental results.

I haven't read this paper carefully yet, but since the authors claim it is the first published account of abstract interpretation for CHRs, I decided to mention it here anyway.

Automatic type inference via partial evaluation

Automatic type inference via partial evaluation. Aaron Tomb, Cormac Flanagan. PPDP’05.

Type checking and type inference are fundamentally similar problems. However, the algorithms for performing the two operations, on the same type system, often differ significantly. The type checker is typically a straightforward encoding of the original type rules. For many systems, type inference is performed using a two-phase, constraint-based algorithm.We present an approach that, given the original type rules written as clauses in a logic programming language, automatically generates an efficient, two-phase, constraint-based type inference algorithm. Our approach works by partially evaluating the type checking rules with respect to the target program to yield a set of constraints suitable for input to an external constraint solver. This approach avoids the need to manually develop and verify a separate type inference algorithm, and is ideal for experimentation with and rapid prototyping of novel type systems.

Also somewhat relevant to the discussions here about type checking as abstract interpretation.

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

XML feed