Lambda the Ultimate

Declarative Networking: Language, Execution and Optimization, Boon Thau Loo, Tyson Condie, Minos Garofalakis, David A. Gay, Joseph M. Hellerstein, Petros Maniatis, Raghu Ramakrishnan, Timothy Roscoe and Ion Stoica.

First, we motivate and formally define the Network Datalog (NDlog) language for declarative network specifications.
Second, we introduce and prove correct relaxed versions of the traditional semi-naive query evaluation technique, to overcome fundamental problems of the traditional technique in an asynchronous distributed setting. Third, we consider the dynamics of network state, and formalize the “eventual consistency” of our programs even when bursts of updates can arrive in the midst of query execution. Fourth, we present a number of query optimization opportunities that arise in the declarative networking context, including applications of traditional techniques as well as new optimizations. Last, we present evaluation results of the above ideas implemented in our P2 declarative networking system, running on 100 machines over the Emulab network testbed.

I will be the first to admit that I somehow fundamentally do not get the logic programming style, but presenting a routing discovery protocol in about eight lines of code is pretty cool.

From the "Whoa!" files:

Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference

This paper addresses the question of how to extend OCaml’s Hindley-Milner type system with types indexed by logical propositions and proofs of the Coq theorem prover, thereby providing an expressive and extensible mechanism for ensuring fine-grained program invariants. We propose adopting the approached used by Shao et al. for certified binaries. This approach maintains a phase distinction between the computational and logical languages, thereby limiting effects and non-termination to the computational language, and maintaining the decidability of the type system. The extension subsumes language features such as impredicative first-class (higher-rank) polymorphism and type operators, that are notoriously difficult to integrate with the Hindley-Milner style of type inference that is used in OCaml. We make the observation that these features can be more easily integrated with type inference if the inference algorithm is free to adapt the order in which it solves typing constraints to each program. To this end we define a novel “order-free” type inference algorithm. The key enabling technology is a graph representation of constraints and a constraint solver that performs Hindley-Milner inference with just three graph rewrite rules.

Another tough-to-categorize one: dependent types, the Curry-Howard Correspondence, logic programming, theorem provers as subsystems of compilers, implementation issues... it's all in here.

Update: A prototype implementation is available here, but it took a bit of Google-fu to find, and it's brand new, so be gentle.

Update II: The prototype implementation isn't buildable out of the box, and includes a complete copy of both the Coq and O'Caml distributions, presumably with patches etc. already applied. So it's clearly extremely early days yet. But this feels very timely to me, perhaps because I've just started using Coq within the past couple of weeks, and got my copy of Coq'Art and am enjoying it immensely.

Update III: It occurs to me that this might also relate to Vesa Karvonen's comment about type-indexed functions, which occurs in the thread on statically-typed capabilities, so there might be a connection between this front-page story and the front-page story on lightweight static capabilities. That thought makes me happy; I love it when concepts converge.

Socially Responsive, Environmentally Friendly Logic
by Samson Abramsky

We consider the following questions: What kind of logic has a natural semantics in
multi-player (rather than 2-player) games? How can we express branching quantifiers, and
other partial-information constructs, with a properly compositional syntax and semantics?
We develop a logic in answer to these questions, with a formal semantics based on multiple
concurrent strategies, formalized as closure operators on Kahn-Plotkin concrete domains.
Partial information constraints are represented as co-closure operators. We address the
syntactic issues by treating syntactic constituents, including quantifiers, as arrows in a
category, with arities and co-arities. This enables a fully compositional account of a wide
range of features in a multi-agent, concurrent setting, including IF-style quantifiers.

This paper seems to unify multiple interesting directions - logic, game semantics, concurrent constraint programming (and concurrent programming in general).

At the same time it remains very accessible, without overwhelming amount of math, so can be hopefully useful not only for academics. I, for one, was waiting for exactly this kind of paper for two years (and my interest is very practical).

Multiplayer Curry-Howard correspondence, anyone? Or Curry-Howard for web services?

The first 10 Prolog Programming Contests took place in Ithaca (1994), Portland (1995), Bonn (1996), Leuven (1997), Manchester (1998), Las Cruces (1999), Paphos (2001), Copenhagen (2002), Mumbay (2003) and Saint-Malo (2004). The contest organisers have written this book, containing the (slightly reworked) questions and an answer (in Prolog of course) for each question... The book is now also freely downloadable on this page.

For your enjoyment...

Nested commits for mobile calculi: extending Join
by Roberto Bruni, Hernan Melgratti, Ugo Montanari

In global computing applications the availability of a mechanism for some form of committed choice can be useful, and sometimes necessary. It can conveniently handle, e.g., contract stipulation, distributed agreements, and negotiations with nested choice points to be carried out concurrently. We propose a linguistic extension of the Join calculus for programming nested commits, called Committed Join (cJoin).
It provides primitives for explicit abort, programmable compensations and interactions between ongoing negotiations. We give the operational semantics of cJoin in the reflexive CHAM style. Then we discuss its expressiveness on the basis of a few examples and of the cJoin encoding of other paradigms with similar aims but designed in different contexts, namely AKL and Zero-Safe nets.

To me the main interest lies in section 4.2, which shows an encoding of a subset of AKL in cJoin.
More references to relationships between logic/constraint and "pi-family" approaches to concurrency are welcome!

Continuations for Parallel Logic Programming
by Eneia Todoran and Nikolaos S. Papaspyrou

This paper gives denotational models for three logic programming
languages of progressive complexity, adopting the
"logic programming without logic" approach. The first language
is the control ow kernel of sequential Prolog, featuring
sequential composition and backtracking. A committed-choice
concurrent logic language with parallel composition
(parallel AND) and don't care nondeterminism is studied
next. The third language is the core of Warren's basic Andorra
model, combining parallel composition and don't care
nondeterminism with two forms of don't know nondeterminism
(interpreted as sequential and parallel OR) and favoring
deterministic over nondeterministic computation. We show
that continuations are a valuable tool in the analysis and
design of semantic models for both sequential and parallel
logic programming. Instead of using mathematical notation,
we use the functional programming language Haskell
as a metalanguage for our denotational semantics, and employ
monads in order to facilitate the transition from one
language under study to another.

This paper happens to combine several topics that interest me lately - AKL (a precursor of Oz), denotational semantics, continuations, and implementing programming languages in Haskell.

If you share at least some of these interests - take a look!

I have been reading a bit of late on Constraint Programming and thought I'd dump some of the links that have helped me along the way. One problem I find with learning Constraint Programming is that I easily get bogged down in the details of implementation and theory. In basic terms, CP consists of a three stage process: (1) Declare the domain (range) of the variables; (2) Declare the constraints on those variables; and (3) Search for solutions. The 1st and 2nd stages can be combined without too much loss, but there seems to be a general consensus that search should be kept separate as much as possible, since it usually is the most expensive and the least declarative. Most of the resources concentrate on the details about how to go about defining programs in these three stages, as well as giving hints about limiting the combinatorial explosion of the search.

The best tutorial I've found is Finite Domain Constraint Programming in Oz which gives a pretty good practical introduction to the subject. Constraint Programming in Alice is a related work in progress that follows the same general outline. For those who like slide presentations, the lecture notes of Christian Schulte and Guido Tack are good resources. Both Christian and Guido are working on the implementation of Gecode, which is a set of libraries (in C++) that seek to take the model of computation spaces, as first realized in Oz, and extend their reach into other programming languages (Christian uses Java, while Guido uses Alice). For a more detailed look, Christian Schulte's PhD thesis on Programming Constraint Services is an in depth treatise on the use of computation spaces for CP.

One book I've been eyeing is Constraint Based Local Search which uses COMET as the PL. My only hesitation is that I don't quite grok the concept of Local Search - a search method that is supposed to be quite efficient but not guaranteed to find a solution. Anyone care to hit me with a clue-by-four on Local Search?

Here's a very simple implementation of Kanren that gives the barest minimum to get the taste of logic programming in very simple Scheme.

I am told that the code was written in about three hours at the meeting of a Functional Programming Group (Toukyou/Shibuya, Apr 29, 2006), as a quick illustration of logic programming.

The code is very easy to read, and the comments are instructive and helpful.

Enjoy!

Typed Concurrent Programming with Logic Variables

We present a concurrent higher-order programming language called Plain and a
concomitant static type system. Plain is based on logic variables and computes
with possibly partial data structures. The data structures of Plain are procedures, cells, and records. Plain's type system features record-based subtyping, bounded existential polymorphism, and access modalities distinguishing between reading and writing.

You may want to compare this with The Oz Programming Model (OPM), which

... is a concurrent programming model subsuming higher-order functional and object-oriented programming as facets of a general model. This is particularly interesting for concurrent object-oriented programming, for which no comprehensive formal model existed until now. The model can be extended so that it can express encapsulated problem solvers generalizing the problem solving capabilities of constraint logic programming.

Another paper on OPM is The Operational Semantics of Oz.

In short, the model of Plain is based on that of Oz with the main differences being:

1. Plain statically types programs using a type system with subtyping, while Oz is latently typed.
2. Therefore Plain chooses to drop support for unification in favor of a single-assignment operation.

A Monadic Semantics for Core Curry

The structure of our semantics sheds some light on how the basic components
of the language interact. In particular, we can see that the addition
of non-determinism, logic variables and narrowing can be accomplished just
by making a suitable shift in interpretation monad. We could emphasize
this modularity further by presenting the relevant monads as compositions of
monad transformers.

While being primarily an "interpreter as semantics" paper, it looks like a nice example of a DSL in Haskell.

As a bonus, it also discusses some features of logic programming.