Lambda the Ultimate

From the abstract of Per Brand's Ph.D. thesis,
The Design Philosophy of Distributed Programming Systems: the Mozart Experience, which has just appeared (dated June 2005):

Distributed programming is usually considered both difficult and inherently different from concurrent centralized programming. It is thought that the distributed programming systems that we ultimately deploy, in the future, when we've worked out all the details, will require a very different programming model and will even need to be evaluated by new criteria.



The Mozart Programming System, described in this thesis, demonstrates that this need not be the case. It is shown that, with a good system design, distributed programming can be seen as an extended form of concurrent programming. This is from the programmer's point-of-view; under the hood the design and implementation will necessarily be more complex. We relate the Mozart system with the classical transparencies of distributed systems. We show that some of these are inherently on the application level, while as Mozart demonstrates, others can and should be dealt with on the language/system level.

[...]

The full range of the design and implementation issues behind Mozart are presented. This includes a description of the consistency protocols that make transparency possible for the full language, including distributed objects and distributed data-flow variables.

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

Gianluigi Ferrari, Eugenio Moggi and Rosario Pugliese

MetaKlaim - a Type Safe Multi-stage Language for Global Computing

This paper describes the design and the semantics of MetaKlaim, an higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and “traditional” computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types ´a la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide are network applications are maintained whenever computations interoperate with potentially untrusted components.

Recovering resources in the pi-calculus

Although limits of resources such as memory or disk usage
are one of the key problems of many communicating applications, most
process algebras fail to take this aspect of mobile and concurrent systems
into account. In order to study this problem, we introduce the Controlled
pi-calculus, an extension of the pi-calculus with a notion of recovery of
unused resources with an explicit (parametrized) garbage-collection and
dead-process elimination. We discuss the definition of garbage-collection
and dead-process elimination for concurrent, communicating applications,
and provide a type-based technique for statically proving resource
bounds. Selected examples are presented and show the potential of the
Controlled pi-calculus.

Since pi calculus is a hot topic lately, Pierce's Foundational Calculi for Programming Languages might be of interest as an introduction. It very briefly introduces and justifies foundational calculi in general, spends about 10 pages on lambda calculus, then builds on that with another 7 pages on pi calculus.

Linear forwarders are actually the basic mechanism of an earlier implementation of the pi calculus called the fusion machine. We modify the fusion machine, replacing fusions by forwarders. The result is more robust in the presence of failures, and more fundamental.

And also:

The point of this paper is to solve the problem of input capability with a language that is “just right” – it neither disallows more features than necessary (as does the join calculus), nor adds more implementation work than is necessary (as does the fusion machine).

Yes, these are the same capabilities as in capability-based security. I am looking forward to read the complete paper, as it seems to confirm my unclear ideas of how capabilities and various pi calculi are related.

This article by Steve Maine argues that SOAP may be used as a canonical form for all varieties of messaging between participants in a distributed system, because they are all isomorphic to each other anyway:

For example, RPC and Messaging have already been shown to be isomorphic models of the same thing. There are similar dualities between "messages sent to a stateful service" and "methods called on a stateful object". All of these ideas are just attempts to build a conceptual model around the interactions between distributed systems. Unfortunately, each of these thought-models carries with it a certain amount of implicit semantic baggage, and that fact has really hampered the development of scalable, widely interoperable distributed systems to date.

I'm not sure if it's a rat I smell, or just my own inherent dislike of SOAP.

Dear Sir, I tried your distributed messaging protocol three years ago, and since then I have used no other...

The Kell Calculus: A Family of Higher-Order Distributed Process Calculi

This paper presents the Kell calculus, a family of distributed process calculi, parameterized by languages for input patterns, that is intended as a basis for studying component-based distributed programming. The Kell calculus is built around a pi-calculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higher-order communication, programmable membranes, and dynamic binding. The paper discusses these principles, and defines the syntax and operational semantics common to all calculi in the Kell calculus family. The paper provides a co-inductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higher-order bisimulation called strong context bisimulation. The paper also contains several examples that illustrate the expressive power of Kell calculi.

NB: a family of calculi, parameterized by languages

See also: The Kell Calculus

In this page you will find information about the current state of the Kell calculus, links to published papers and drafts, information about where the Kell calculus is going[...]

This discussion over on the Haskell Mailing List might interest those readers following the debates on concurrency issues in the discussion group...

We mentioned O'Haskell previously on LtU, but a recent discussion of OOP vs. FP vs. everything made be to believe that it's worth to remember this (unfortunately unsupported) programming language.

It's instructive to read the rationale for this PL, as it helps to see how OOP and FP solve similar tasks in orthogonal (or just different) ways.

Note that the author of O'Haskell abandoned it in favor of Timber.