A Tail-Recursive Machine with Stack Inspection

A Tail-Recursive Machine with Stack Inspection. John Clements and Matthias Felleisen, TOPLAS 2004.

Security folklore holds that a security mechanism based on stack inspection is incompatible with a global tail call optimization policy... In this article, we prove this widely held belief wrong. ... Our machine is surprisingly simple and suggests that tail calls are as easy to implement in a security setting as they are in a conventional one.

I don't believe we've discussed this paper before, although it was mentioned in this thread. Tail calls have been a topic of discussion here several times. [1][2][3]

Rho calculus

The Rho-calculus is a calculus of pattern matching that embeds the lambda-calculus in a very simple manner, and also naturally accomodates a number of extensions of the lambda-calculus. It encodes the results of pattern matching in a manner that ensures confluence of the whole calculus.

It was proposed by Horatiu Cirstea and Claude Kirchner in 1998, and Matching Power, a 2001 RTA paper, is maybe the nicest introduction to the calculus. Kirchner's research group maintains a list of papers.

Postscript There was an LtU classic story on the rho-calculus as well...

Semantic Distance: NLP Not a Resource Sink

Following the story on Mind Mappers and other RDF comments of late, I thought this NLP slide show (PDF) should get a story. Dr. Adrian Walker offers an interesting perspective in a friendly crayon-colored format, including a critique of RDF. Source site Internet Business Logic has other offerings including an online demo.

Module Mania: A Type-Safe, Separately Compiled, Extensible Interpreter

Module Mania: A Type-Safe, Separately Compiled, Extensible Interpreter

To illustrate the utility of a powerful modules language, this paper presents the embedded interpreter Lua-ML. The interpreter combines extensibility and separate compilation without compromising type safety. Its types are extended by applying a sum constructor to built-in types and to extensions, then tying a recursive knot using a two-level type; the sum constructor is written using an ML functor. The initial basis is extended by composing initialization functions from individual extensions, also using ML functors.

This is an excellent example of how the ML module language doesn't merely provide encapsulation but also strictly adds expressive power. It also demonstrates how a dynamic language (Lua) can be embedded in the statically-typed context of ML. Finally, it demonstrates that none of this need come at the expense of separate compilation or extensibility. Norman Ramsey's work is always highly recommended.

ClassicJava in PLT Redex

Classic Java

This collection is an implementation of (most of) ClassicJava, as defined
in "A Programmer's Reduction Semantics for Classes and Mixins," by Matthew
Flatt, Shriram Krishnamurthi, and Matthias Felleisen; in _Formal Syntax and
Semantics of Java_, Springer-Verlag LNCS 1523, pp. 241-269, 1999. A
tech-report version of the paper is also available at
< The implementation is
written in PLT Redex, also available through PLaneT. Please consult that
package's documentation for further details.

This might be interesting to folks curious about how to formalize a real language, or about how PLT Redex works in practice.

What good is Strong Normalization in Programming Languages?

There's a neat thread about strong normalization happening on The Types Forum.

If you've ever wondered Why is it useful to have {type systems,reductions,operations,...} that always terminate? this may Illuminate you.
Here are some snippets to give you a feel for the discussion:

I think it is clearer to split Gérard's original question in two:

  1. Is strong normalization useful for programming languages ?
  2. Is the proof of strong normalization via type systems applicable for programming languages?

-- François-Régis Sinot

Termination is good:

If a program is a solution to a problem then knowing that it terminates
for any input is an important aspect of it being a solution. Often the
best way to see that it is terminating is expressing it in a language
where all programs terminate. The programming language Epigram is an
example of an experimental language which is intended to be terminating
(even though not all conditions are enforced in the current version), see for more information.

-- Thorsten Altenkirch

Termination is good!

I think the moral sense of strong normalization is that a program
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like
iteration, recursion etc. My favourite example here is that the
"big Omega" can be written in Algol 60, because procedure types
in this language are not fully specified.

-- Pawel Urzyczyn

Termination is good and with fixpoints is turing complete?

Another way to put this is that data structures should be definable in a
strongly-normalising language so that data access, etc. is guaranteed to
terminate. Then add fixpoints or loops to describe arbitrary computations.

-- Barry Jay

Terminating reductions allows exhaustive applications of optimizations:

In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the classical SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ).

-- Andrew Kenney

Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list.

Mechanizing Language Definitions

The problem: Most languages don't have formal specifications.

The solution (maybe): Make specification easier by using mechanized tools (for example, use Twelf).

The presentation: here (Robert Harper, ICFP'05).

The conclusion: You decide.

Zipper-based file server/OS

We present a file server/OS where threading and exceptions are all realized via delimited continuations. We use zipper to navigate within any term. If the term in question is a finite map whose keys are strings and values are either strings or other finite maps, the zipper-based file system looks almost the same as the Unix file system. Unlike the latter, however, we offer: transactional semantics; undo of any file and directory operation; snapshots; statically guaranteed the strongest, repeatable read, isolation mode for clients; built-in traversal facility; and just the right behavior for cyclic directory references.

We can easily change our file server to support NFS or 9P or other distributed file system protocol. We can traverse richer terms than mere finite maps with string keys. In particular, we can use lambda-terms as our file system: one can cd into a lambda-term in bash.

The implementation of ZFS has no unsafe operations, no GHC let alone Unix threads, and no concurrency problems. Our threads cannot even do IO and cannot mutate any global state --- and the type system sees to it. We thus demonstrate how delimited continuations let us statically isolate effects even if the whole program eventually runs in an IO monad.

zfs-talk: Expanded talk with the demo. It was originally presented as an extra demo at the Haskell Workshop 2005

ZFS.tar.gz: The complete source code, with comments. It was tested with GHC 6.4 on FreeBSD and Linux

From: Zipper-based file server/OS

Neat, a referentially transparent filesystem with transactional semantics in 540 lines of Haskell. I can think of some interesting uses for this.

The essence of Dataflow Programming by Tarmo Uustalu and Varmo Vene

The Essence of Dataflow Programming

The abstract:

We propose a novel, comonadic approach to dataflow (streambased) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure context-dependent computation. In particular, we develop a generic comonadic interpreter of languages for context-dependent computation and instantiate it for stream-based computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and context-dependent computation. We apply the latter to analyse clocked dataflow (partial streams based) computation.

If you've ever wondered about dataflow or comonads, this paper is a good read. It begins with short reviews of monads, arrows, and comonads and includes an implementation. One feature that stood out is the idea of a higher-order dataflow language.

XML feed