Compiling Exceptions Correctly

Exceptions are an important feature of modern programming languages, but their compilation has traditionally been viewed as an advanced topic. In this article we show that the basic method of compiling exceptions using stack unwinding can be explained and verified both simply and precisely, using elementary functional programming techniques. In particular, we develop a compiler for a small language with exceptions, together with a proof of its correctness.

The PROSPER Toolkit

The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treated as components. A system incorporating such tools becomes another component that can be embedded in an application. This paper describes the PROSPER Toolkit which enables this. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit.

A Tutorial on the Universality and Expressiveness of Fold

In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the universal property of fold both as a proof principle that avoids the need for inductive proofs, and as a definition principle that guides the transformation of recursive functions into definitions using fold. Secondly, we show that even though the pattern of recursion encapsulated by fold is simple, in a language with tuples and functions as first-class values the fold operator has greater expressive power than might first be expected.

Calculating an Exceptional Machine

In previous work we showed how to verify a compiler for a small language with exceptions. In this article we show how to calculate, as opposed to verify, an abstract machine for this language. The key step is the use of Reynold's defunctionalization, an old program transformation technique that has recently been rejuvenated by the work of Danvy et al.

The Sparta and the Athens Of Our Age At Daggers Drawn: Polities, Perceptions, and Peace

While historically notions of democracy have varied widely, democratic peace theory has generally defined it in procedural terms. This article takes a close look at the Anglo-French confrontation of 1840. I show that while leaders on both sides were prepared to risk war to gain bargaining advantages, only the French left really wanted to fight. Why? By today's criteria, Britain was incontestably more democratic, with its monarch's powers far more restricted and its suffrage several times as large. Nevertheless, both sides considered France more democratic, with French republicans despising Britain as an aristocratic oligarchy. While Spencer Weart is right to argue that democratic republics may be hostile to oligarchic ones, they will not necessarily define each other according to modern procedural criteria. Instead, they may judge regimes by the broader social structures that shape power relationships and by outcomes, possibly explaining wars or near misses between democracies.

Extracting reusable document components for variable data printing

Variable Data Printing (VDP) has brought new flexibility and dynamism to the printed page. Each printed instance of a specific class of document can now have different degrees of customized content within the document template. This flexibility comes at a cost. If every printed page is potentially different from all others it must be rasterized separately, which is a time-consuming process. Technologies such as PPML (Personalized Print Markup Language) attempt to address this problem by dividing the bitmapped page into components that can be cached at the raster level, thereby speeding up the generation of page instances. A large number of documents are stored in Page Description Languages at a higher level of abstraction than the bitmapped page. Much of this content could be reused within a VDP environment provided that separable document components can be identified and extracted. These components then need to be individually rasterisable so that each high-level component can be related to its low-level (bitmap) equivalent. Unfortunately, the unstructured nature of most Page Description Languages makes it difficult to extract content easily. This paper outlines the problems encountered in extracting component-based content from existing page description formats, such as PostScript, PDF and SVG, and how the differences between the formats affects the ease with which content can be extracted. The techniques are illustrated with reference to a tool called COG Extractor, which extracts content from PDF and SVG and prepares it for reuse.