Theory

Principles of Program Analysis

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

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

RDF Elevator Pitch

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

Haskell Communities and Activities Report, Seventh Edition, November 2004

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: Shift to Control

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 tutorial on graph transformation

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.

SAT 3 Proof with E Prover via OWL

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.

Logical Methods in Computer Science

Logical Methods in Computer Science is a fully refereed, open access, free, electronic journal. It welcomes papers on theoretical and practical areas in computer science involving logical methods, taken in a broad sense... Papers are refereed in the traditional way, with two or more referees per paper. Copyright is retained by the author.

Many of the topics to be covered by this new journal are related to PL research or are of interest to PL researchers, so I hope many of the papers published in it will be interesting enough to discuss here.

The editorial team is impressive, with Dana Scott as editor-in-chief, and Plotkin and Vardi as managing editors.

The editorial board includes many prominent figures among them Abadi, Abramsky, Gries, Pierce, Wadler and Wand.

Retrospective: The Essence of Compiling with Continuations

(link)

From 20 years of the ACM SIGPLAN Conference on Programming Language Design and Implementation: 1979 - 1999. A Selection.

A one page retrospective of this highly important paper. Useful as a guide to the literature and related research.

XML feed