Lambda the Ultimate

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.

The report (by Oleg Kiselyov) shows that shift, control, shift0, etc. delimited continuation operators are macro-expressible in terms of each other. The report thus confirms the result first established by Chung-chieh Shan in Shift to Control. The operators shift, control, control0, shift0 are the members of a single parameterized family, and the standard CPS is sufficient to express their denotational semantics.

The report uses a more uniform method and it formally proves that 'control' implemented via 'shift' indeed has its standard reduction semantics. It is common knowledge that first-class continuations are quite tricky -- and delimited continuations are trickier still. Therefore, a formal proof is a necessity.

On the practical side, the report shows the simplest known Scheme implementations of control, shift0 and control0 (similar to `cupto'). The method in the report lets us design 700 more delimited control operators, which compose stack fragments in arbitrary ways.

I love this sort of thing, and since section 4 includes Scheme code, you can try to skip the theory if you find it intimidating.

I know this stuff can look a bit hairy. If there's interest, I hope Oleg would agree to help people new to this sort of material in understanding sections 2 and 3. But you have to ask nicely...

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.

(via TYPES)

How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? To gauge progress in this area, we issue here a set of challenge problems, dubbed the POPLmark Challenge, chosen to exercise many aspects of programming languages that are known to be difficult to formalize.

A valid solution to the challenge will consist of appropriate software tools, a language representation strategy, and a demonstration that this infrastructure is sufficient to formalize the challenge problems.

The POPLmark team explains,

We are not ourselves automated reasoning experts but rather potential users; our impression is that current tools are almost at the point where they can be used routinely. It's time to bring mechanized metatheory to the masses - go to it!

Pitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001.

In the lambda calculus, the particular choice of variable names - even free variables - is irrelevant. Names serve two purposes:

• as mnemonics to help human readers understand their role, and
• to distinguish variables that are meant to be different and unify variables that are meant to be the same.

In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with capture-avoiding substitution, the Barendregt variable convention, gensym, and the like. These are all ways of getting around the fact that we've committed to a particular name when we really shouldn't have cared what the name was.

There are several standard ways to deal with this. Generating fresh names with gensym is awkward and forces the implementer to reimplement binding and substitution from scratch for each new object language; not to mention its violation of referential transparency. de Bruijn indices remove the variable names but are hard to read and understand. Higher-order abstract syntax implements binders in the object language as functions in the metalanguage, in order to reuse the built-in mechanisms of binding and substitution; but by mixing higher-order values in algebraic datatypes, structural induction is hard to recover.

This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOAS-like notation for introducing binders into an abstract syntax. This is the set-theoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past.

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.

Aspect-oriented programming is emerging as a powerful tool for system design and development. In this paper, we study aspects as primitive computational entities on par with objects, functions and horn-clauses. To this end, we introduce μABC, a name-based calculus, that incorporates aspects as primitive. In contrast to earlier work on aspects in the context of object-oriented and functional programming, the only computational entities in μABC are aspects. We establish a compositional translations into μABC from a functional language with aspects and higher-order functions. Further, we delineate the features required to support an aspect-oriented style by presenting a translation of μABC into an extended π-calculus.

Greg Restall is

writing a book, entitled Proof and Counterexample (or PnC for short). It's on logic viewed through the lens of proof theory. In particular, it covers natural deduction, sequent calculus, normalisation and cut-elimination. It's designed to both be state-of-the-art reseearch on these topics, together with an introduction appropriate for an advanced undergraduate. (We'll see how that works. I'll be test-driving the material with honours students from February to June in 2005.)

These pages will contain all sorts of different material about the book: comments, discussion, pointers to related material, and anything else that the community behind this site sees fit to write.

Newcomers to the field might wonder why this is relevant to programming languages, and some readers would regard this as pointless theory...

But if you are one of us guys excited by Curry-Howard, you might enjoy this wiki a lot.

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

Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculus

The Asynchronous pi-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the pi-calculus which contains no explicit operators for choice and output-prefixing. The communication mechanism of this calculus, however, is powerful enough to simulate output-prefixing, as shown by Boudol, and input-guarded choice, as shown recently by Nestmann and Pierce. A natural question arises, then, whether or not it is possible to embed in it the full pi-calculus. We show that this is not possible, i.e. there does not exist any uniform, parallel-preserving, translation from the pi-calculus into the asynchronous pi-calculus, up to any “reasonable” notion of equivalence. This result is based on the incapablity of the asynchronous pi-calculus of breaking certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the pi-calculus and CCS.

Quite an important result for those who care about pi.

The others may just enjoy the use of symmetry in the proof.

As CiteSeer is down this weekend, I used a link to CiteBase.

[on edit: CiteSeer is back]