Lambda the Ultimate

A screencast about Microsoft's Atlas toolkit (Flash, Windows Media and QuickTime formats available).

Atlas it ASP.Net's AJAX solution, and it seems quite well thought out from what I can tell.

Both the ASP.Net Atlas code and the Atlas XML Script DSL provide a declarative programming model, which should help build AJAX applications which otherwise require a somewhat confusing programming model for beginners.

It sohuld be interesting to see how this approach compares with web frameworks such as Rails (whose DWIM approach makes it quite DSL-ish), and with the approach Wadler takes with Links.

Uniform Proofs as a Foundation for Logic Programming (Dale Miller, Gopalan Nadathur, Frank Pfenning & Andre Scedrov 1989/1991) introduces the concept of unirform provability, which is fundamental to abstract logic programming, which in turn drives much of the more principled work in modern logic programming.

In particular, this paper (i) shows that logics that support uniform provability support goal-directed proof search, and so may be used as the foundation of a logic programming language, and (ii) the notion of uniform provability may be used to explore new forms of logic programming, in particular introducing the class of hereditary Harrop formulae which underlies lambda-Prolog. A classic...

Abstract logic programming is expored in a more introductory manner in this paper.

Via the plt-scheme mailing list:

We are pleased to announce the first public release [beta 7] of ACL2
in DrScheme, a combination of the ACL2 theorem prover system with the
DrScheme programming environment. The objective of this project is
to provide a development environment for ACL2 suitable for novice
users as well as enhancements of ACL2 that are attractive for the
typical undergraduate student (graphics, interactive games, sound).

There's a tutorial with screenshots and some examples on the ACL2 in DrScheme web page.

I'm always happy to see reasoning about programs introduced at the undergraduate level. I wonder what the LtU community would do with a tool like this. What cool things would you teach with a beginner's theorem prover?

I will not quote this introduction/manifesto/historical overview, as every page of it is worth reading.

It is not only a nice introduction into a promising field, but also a demonstration of how language design issues can be (to some extent) separated from high-level fundamental intuitions.

It is also quite interesting to follow the historical lines of the paper, it reads like an epic!

Ah, and by the way, that's the same constraint programming that underlies Oz.

Guess what I stumbled across at my local bookstore?

Previously mentioned on LtU, and now available... When the book was announced, Ehud said:

Authored by two of my favorites, Dan Friedman and Oleg, I have such high expectations, that however great the book is going to be, I am sure to be disappointed...

After working through the first five chapters (and sneaking a look at the implementation at the end), I'm pleased to announce that no one is likely to be disappointed... It's a real tour de force.

As expected, the focus this time is logic programming, in the form of a new set of primitives elegantly implemented around a backtracking monad in Scheme. Of course the format is familiar and comfortable, and of course it's charmingly illustrated by Duane Bibby.

So, get your copy today, and congratulations to the authors on a job well done!

Propositional Satisfiability (SAT) and Constraint Programming (CP) have developped as two relatively independent threads of research, cross-fertilising occasionally. These two approaches to problem solving have a lot in common, as evidenced by similar ideas underlying the branch and prune algorithms which are most successful at solving both kinds of problems. They also exhibit differences in the way they are used to state and solve problems, since SAT's approach is in general a black-box approach, while CP aims at being tunable and programmable. This report overviews the two areas in a comparative way, emphasizing the similarities and differences between the two and the points where we feel that one technology can benefit from ideas or experience acquired from the other.

This is a long and detailed survey, that may serve as an introduction to the two fields.

How useful these searching strategies are as programming language constructs is open to debate, of course.

It rapidly became clear that a single language runtime is too limited for general applications ... as a minimum we needed both a linear-flow language and a recursive tree composition language ... while declarative languages are excellent for rapid assembly of XML operations, they are terrible for expressing business logic and logical flow-control ... Our other declarative language is XML Recursion Language (XRL). XRL is like XInclude with services, in which inclusion references fire service invocations into the URI address space in order to recursively compose an XML document. XRL is an elegant and powerful way of building XHTML applications ... The active URI, in combination with the local NetKernel environment, is a functional program - Introducing NetKernel.

Main site; Tour.

It's another XML pipeline (there's a Freshmeat project that lets Coccoon apps run in NetKernel), apparently from HP, which might interest people here.

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. We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a new dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

Another "extreme" use of static typing...

The Essence of Dataflow Programming

The abstract:

We propose a novel, comonadic approach to dataflow (streambased) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure context-dependent computation. In particular, we develop a generic comonadic interpreter of languages for context-dependent computation and instantiate it for stream-based computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and context-dependent computation. We apply the latter to analyse clocked dataflow (partial streams based) computation.

If you've ever wondered about dataflow or comonads, this paper is a good read. It begins with short reviews of monads, arrows, and comonads and includes an implementation. One feature that stood out is the idea of a higher-order dataflow language.

The Andorra Kernel Language (AKL) is introduced. It is shown how AKL provides the programming paradigms of both Prolog and GHC. This is the original goal of the design. However, it has also been possible to provide capabilities beyond that of Prolog and GHC. There are means to structure search, more powerful than plain backtracking. It is possible to encapsulate search in concurrent reactive processes. It is also possible to write a multi-way merger with constant delay. In these respects AKL is quite original. Although AKL is an instance of our previously introduced Kernel Andorra Prolog framework, this exposition contains important extensions, and a considerable amount of unnecessary formal overhead has been stripped away.

While not the latest word in its area (published in 1991), it is well worth reading (and I don't remember seeing links to it on LtU).