Lambda the Ultimate

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]

To coincide with the reprinting of Principles of Program Analysis by Flemming Nielson, Hanne Riis Nielson and Chris Hankin the authors launched a new web page containing lecture slides and other supplementary material.

The lecture slides cover things like data flow analysis, control flow analysis and abstract interpretation.

Non-determinism in functional languages. Sondergaard and Sestoft. The Computer Journal, Volume 35, Issue 5, pp. 514-523. 1992

The introduction of a non-deterministic operator in even an very simple functional programming language gives rise to a plethora of semantic questions. These questions are not only concerned with the choice operator itself. A surprisingly large number of different parameter passing mechanisms are made possible by the introduction of bounded non-determinism. The diversity of semantic possibilities is examined systematically...

A very useful paper if you are interested in this sort of thing. Thinking of non-determinism helps calrify muddled thinking about properties such as referential transparency.

The version I found online, alas, is a set of tiff image files, one for each page...

Eureka, the perfect RDF introduction with thanks to A.M. Kuchling (amk). Nothing beats crayon-colored diagrams. It is short, sweet, and hits the main points precisely, including 'political' issues at the end. Much W3C advocacy makes the Semantic Web sound too futuristic....The RDF Core spec is hard to read and really boring....Introductory tutorials are few....Simple things can be done without much effort, and can still be useful.

On one island are the semantic web folks. On another island are semantic filesystem folks. A summit seems in order. I don't hear much about the two working together, but then I live on yet another island. RDF+ReiserFS looks like a match made in heaven, for example, Reiser4 uses dancing trees, which obsolete the balanced tree algorithms used in databases...Do you want a million files in a directory, and want to create them fast? No problem.

From the article,

Reiser has "substantial plans" for adding new kinds of semantics to ReiserFS to help it challenge Microsoft's efforts. "We're planning on competing with the Longhorn filesystem," he says.

The new ReiserFS will eschew the relational algebra approach and work with semistructured data. "The person entering data can employ [the] structure inherent in the data rather than forcing a structure," Reiser said, adding, "Flexibility in querying and creating data is our target. [This] will stand in contrast to Microsoft's SQL-based approach, which does not have that flexibility."

The November 2004 edition of the biannual Haskell Communities and Activities Report has been published. Lots of new stuff in the last six months, and some old stuff updated as well. The HC&AR has been steadily growing over the last three years, showing that FP is gaining users both professional and private.

Several of the HC&AR items are interesting enough to have their own LtU stories, which may appear shortly.

Ken Shan's Shift to Control (slides) presented at the recent Scheme workshop.

Ken shows that shift/reset, prompt/control, prompt/cupto and lots of other delimited continuation operators are all equally expressible, and all can be modeled by ordinary CPS.

The paper shows that shift and reset can macro-express control and prompt, as well as the other operators, without capturing undelimited continuations or keeping mutable state. This translation is previously unknown in the literature.

Good stuff! But keep in mind that, as the cartoon in the slide says, control operators can make your head hurt...

A nice application of category theory to computer science that is rather simpler than its application to semantics tends to get is the single and double pushout approach to graph transformation. Categorical pushouts allow patterns and rewrites on many kinds of structure, in particular graphs, to be specified in a simple manner. The theory can be read forwards, generalising term rewriting systems to graph rewriting systems, or backwards, specifying parsing problems for a graph grammar.

There's a shortage of good introductory material to this idea online. Offline I can recommend Tutorial introduction to the algebraic approach of graph grammars based on double and single pushouts [citeseer]. Online I suggest Practical Use of Graph Rewriting, and I welcome other suggestions.

An interesting little Semantic Web-related development reported by Jos De Roo (creator of the Java/C# Euler inference engine). He's got the E Prover (an equational theorem prover for clausal logic), to find a proof for the OWL (Web Ontology Language) test case "inconsistent502" (RDF, variations), which is a Description Logic encoding of one of the classic SAT 3 problems.