Lambda the Ultimate

Logfun is a library of logic functors. A logic functor is a function that can be applied to zero, one or several logics so as to produce a new logic as a combination of argument logics. Each argument logic can itself be built by combination of logic functors. The signature of a logic is made of a parser and a printer of formulas, logical operations such as a theorem prover for entailment between formulas, and more specific operations required by Logical Information Systems (LIS). Logic functors can be concrete domains like integers, strings, or algebraic combinators like product or sum of logics.

Logic functors are coded as Objective Caml modules. A logic semantics is associated to each of these logic functors. This enables to define properties of logics like the consistency and completeness of the entailment prover, and to prove under which conditions a generated entailement prover satisfies these properties given the properties of argument logics.

Logic Functors form a framework for specifying new logics, and deriving automatically theorem provers and consistency/completeness diagnoses. Atomic functors are logics for manipulating symbols and concrete domains, while other functors are logic transformers that may add connectives or recursive structures, or may alter the semantics of a logic. The semantic structure of the framework is model theoretic as opposed to the verifunctional style often used in classical logic. This comes close to the semantics of description logics, and we show indeed that the logic ALC can be rebuilt using logic functors. This offers the immediate advantage that variants of ALC can be explored and implemented almost for free.

The use of OCaml functors here may be interesting even for those who aren't into logic languages. The system allows new logics to be created in OCaml itself, by simply composing OCaml functors. This is covered further in Implementation as ML Functors. The quickest way to get a feel for what this system does is to look at the examples.

A Stepper for Scheme Macros. Ryan Culpepper, Matthias Felleisen.

In this paper, we present a macro debugger with full support for modern Scheme macros. To construct the debugger, we have extended the macro expander so that it issues a series of expansion events. A parser turns these event streams into derivations in a natural semantics for macro expansion. From these derivations, the debugger extracts a reduction-sequence (stepping) view of the expansion. A programmer can specify with simple policies which parts of a derivation to omit and which parts to show. Last but not least, the debugger includes a syntax browser that graphically displays the various pieces of information that the expander attaches to syntactic tokens.

Another paper from the Scheme workshop.

Apart from being a nice exercise for macro lovers, a good macro debugger is essential for lowering the barrier to macro programming. Since macro programming is an important technique for building DSELs and for language oriented programming in general, having better macro debugging facilities is a Good Thing.

SecPAL: Design and Semantics of a Decentralized Authorization Language. Moritz Y. Becker; Andrew D. Gordon; Cédric Fournet. September 2006

We present a declarative authorization language. Policies and credentials are expressed using predicates defined by logical clauses, in the style of constraint logic programming. Access requests are mapped to logical authorization queries, consisting of predicates and constraints combined by conjunctions, disjunctions, and negations. Access is granted if the query succeeds against the current database of clauses. Predicates ascribe rights to particular principals, with flexible support for delegation and revocation. At the discretion of the delegator, delegated rights can be further delegated, either to a fixed depth, or arbitrarily deeply.

Our language strikes a fine balance between semantic simplicity, policy expressiveness, and execution efficiency. The semantics consists of just three deduction rules. The language can express many common policy idioms using constraints, controlled delegation, recursive predicates, and negated queries. We describe an execution strategy based on translation to Datalog with constraints and table-based resolution. We show that this execution strategy is sound, complete, and always terminates, despite recursion and negation, as long as simple syntactic conditions are met.

The SecPAL project lives here (MSR). The project aims are to develop a language for expressing decentralized authorization policies, and to investigate language design and semantics, as well as related algorithms and analysis techniques.

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.

The CellML language is an open standard based on the XML markup language. CellML is being developed by the Bioengineering Institute at the University of Auckland and affiliated research groups.

The purpose of CellML is to store and exchange computer-based mathematical models. CellML allows scientists to share models even if they are using different model-building software. It also enables them to reuse components from one model in another, thus accelerating model building.

Although CellML was originally intended for the description of biological models, it has a broader application (for an example, see the Mooney-Rivlin Constitutive Material Law). CellML includes information about model structure (how the parts of a model are organizationally related to one another), mathematics (equations describing the underlying processes) and metadata (additional information about the model that allows scientists to search for specific models or model components in a database or other repository).

An interesting XML based DSL, with a strong visual programming layer. I don't think we mentioned it in the past, and I'll be happy to hear what people here think of it.

For the recored, I am speaking at the annual conference of the open source community here in Israel, this Friday. My talk is about e-learning, and cellML is one of the examples I am going to discuss.

This blog aims to address all aspects of DSL development, focussing particularly on DSLs embedded in Ruby.

If our DSL department isn't enough for you, you might want to check out this newcomer.

While you wait to see how this blog turns out, you might want to browse our DSL archive: here and here (we also have a fairly empty Ruby department, by the way). After all, we've been doing this for nearly six years now!

Welcome to blogosphere, Dave & Tobias!

While on the subject of quantum computing, I think some of you might enjoy playing with this Scheme DSEL for quantum computation from André van Tonder.

Inform 7 is a radical revision of Graham Nelson's Inform language for interactive fiction (such as Zork). Whereas Inform 6 and its predecessors were (IMO) very low-level languages with a C-like syntax, Inform 7 is a relational language based on natural language syntax and a semantics based on predicate logic. Nelson describes Inform 7 in his usual erudite style, in:

Graham Nelson. Natural Language, Semantic Analysis and Interactive Fiction. 2005.

The Inform 7 implementation comes with a slick graphical interface (currently available for Mac OS X and Windows), and adopts the metaphor of a book, as indeed do aspects of the language itself.

Well worth taking a look at it.

(Credit to Peter J. Wasilko, from whose forum post on Human Factors I cherry-picked this link.)

Hop, A Language for Programming the Web 2.0

From the abstract:

"Hop is a new higher-order language designed for programming interactive web applications such as web agendas, web galleries, music players, etc. It exposes a programming model based on two computation levels. The first one is in charge of executing the logic of an application while the second one is in charge of executing the graphical user interface. Hop separates the logic and the graphical user interface but it packages them together and it supports strong collaborations between the two engines. The two execution flows communicate through function calls and event loops. Both ends can initiate communications."

It appears to be implemented in Scheme. The Hop website has a nice demo.

Benjamin C. Pierce. The Weird World of Bi-Directional Programming, March 2006. ETAPS invited talk.

This nice set of slides (related to Harmony) begins with a detailed exploration of the design space for lenses (the bi-directional constructs), which is quite fun even if you aren't interested in the the rest of the presentation.

It's hard to convey to people what language design is about. I think these slides are a nice example. The process includes exploring various use cases, trying to come up with reasonable semantics, and specifying these decisions formally.

Don't worry: Types are part of the story, as well...