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.

In the beginning was game semantics

In the beginning was game semantics

Giorgi Japaridze

[...] the story and philosophy of computability logic (CL) [...]
According to its philosophy, syntax — the study of axiomatizations or any other, deductive or nondeductive string-manipulation systems — exclusively owes its right on existence to semantics, and is thus secondary to it. CL believes that logic is meant to be the most basic, general-purpose formal tool potentially usable by intelligent agents in successfully navigating real life. And it is semantics that establishes that ultimate real-life meaning of logic. Syntax is important, yet it is so not in its own right but only as much as it serves a meaningful semantics, allowing us to realize the potential of that semantics in some systematic and perhaps convenient or efficient way.
the philosophy of CL relies on two beliefs that, together, present what can be considered an interactive version of the Church-Turing thesis:
Belief 1.
The concept of static games is an adequate formal counterpart of our intuition of ("pure", speed-independent) interactive computational problems.
Belief 2.
The concept of winnability is an adequate formal counterpart of our intuition of algorithmic solvability of such problems.
I already posted links to papers of Giorgi Japaridze several times, but most of them were pretty technical, and also that was before the latest expansion of LtU's readership.

In short, CL is about trying to generalize traditional (both classical and intuitionistic) logic beyond batch computation (well, I hope everybody knows why logic is relevant to computation, if not - look for Curry-Howard isomorphism, or CHI). There are several approaches to doing that, but Giorgi believes they go the wrong way by trying to build upon the syntax, while it's semantics that is primary.

If you believe that computation is more than calculating a function, and that logic is a good way to understand computation - then I recommend to read at least the introduction and the references' list of this paper (the paper is a single chapter for a book, would love to see the whole book).

Combining computational effects

While some researchers seek to generalize monads (to arrows), others try to narrow the focus to achieve a richer theory (and probably deeper understanding).

Combining computational effects: commutativity and sum

We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's side-effects monad transformer (an application is the combination of side-effects with nondeterminism). And we give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application is the combination of exceptions with other effects).
A longer version: Combining Effects: Sum and Tensor

An Operational Semantics for R5RS Scheme

Jacob Matthews and Robby Findler bring us An Operational Semantics for R5RS Scheme (also available in PostScript):

This paper presents an operational semantics for the core of Scheme. Our specification improves over the existing R5RS denotational specification in four ways:

  1. It is more complete, since it contains eval, quote, and dynamic-wind.
  2. It models multiple values in a way that does not require changes to unrelated parts of the language.
  3. It provides a more faithful model of Scheme's undefined order of evaluation.
  4. It is executable, because it is encoded as a program in PLT Redex, a domain-specific language for writing operational semantics.

The executable specification allows others to experiment with our specification and allows us to build a specification test suite, which improves our confidence that our system is a faithful model of Scheme. In addition to contributing a specification of Scheme, this paper presents several novel modeling techniques for Felleisen Hieb-style rewriting semantics that we discovered while developing our R5RS Scheme semantics. All are applicable to a wider range of problems than the specific uses we have for them, and the fact that they combine seamlessly in our full R5RS model shows that they scale to real languages.

This looks like excellent work, as we've come to expect from the PLT folk.

The PLT Redex tool was previously discussed on LtU. If you're interested in checking it out, this page provides links to "everything you need to run PLT Redex and executable versions of every reduction system in the paper".

To be presented at the 2005 Workshop on Scheme and Functional Programming, Tallinn, Estonia, 24 September, 2005.

Thanks to Jens Axel Søgaard for bringing this paper to my attention.

A Typed, Compositional Logic for a Stack-Based Abstract Machine

A Typed, Compositional Logic for a Stack-Based Abstract Machine. Nick Benton. MSR-TR-2005-84. June 2005.

We define a compositional program logic in the style of Floyd and Hoare for a simple, typed, stack-based abstract machine with unstructured control flow, global variables and mutually recursive procedure calls. Notable features of the logic include a careful treatment of auxiliary variables and quantification and the use of substructural typing to permit local, modular reasoning about program fragments. Semantic soundness is established using an interpretation of types and assertions defined by orthogonality with respect to sets of contexts.

Also related to PCC, TAL etc.

Revisiting coroutines

Revisiting coroutines

This paper defends the revival of coroutines as a general control abstraction. After proposing a new classification of coroutines, we introduce the concept of full asymmetric coroutines and provide a precise definition for it through an operational semantics. We then demonstrate that full coroutines have an expressive power equivalent to one-shot continuations and one-shot partial continuations. We also show that full asymmetric coroutines and one-shot partial continuations have many similarities, and therefore present comparable benefits. Nevertheless, coroutines are easier implemented and understood, specially in the realm of procedural languages. Finally, we provide a collection of programming examples that illustrate the use of full asymmetric coroutines to support direct and concise implementation of several useful control behaviors, including cooperative multitasking.

Taking into account real or imaginary interest to control operators on LtU, I believe this paper makes nice reading. See also Coroutines in Lua.

A Monadic Framework for Subcontinuations

A Monadic Framework for Subcontinuations

Functional and delimited continuations are more expressive than traditional
abortive continuations and they apparently seem to require a framework
beyond traditional continuation or monadic semantics. We show that this is not the
case: standard continuation semantics is sufficient to explain directly the common
control operators for delimited continuations. This implies a monadic framework for
typed and encapsulated functional and delimited continuations which we design and
implement as a Haskell library.

XQuery 1.0 and XPath 2.0 Formal Semantics - Last Call

(via Michael Rys)

This is a Last Call Working Draft. Comments on this document are due no later than 15 July 2005...

I guess that those interested in this area know about this, and for others it is a bit too late to get involved, but at least it's good to know the status of the formal specification.

On Evaluation Contexts, Continuations, and the Rest of Computation

Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.

On Evaluation Contexts, Continuations, and the Rest of Computation

Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuations-as-evaluation-contexts are the defunctionalized representation of the continuation of a single-step reduction function and that continuations-as-the-rest-of-thecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single-step reducer. The only difference is how these evaluation contexts are interpreted: a ‘plug’ interpretation yields one-step reduction, whereas a ‘refocus’ interpretation yields evaluation.
XML feed