Lambda the Ultimate

To quote Richard Zach:

CSLI Lecture Notes are now part of the Stanford Medieval and Modern Thought Digitization Project. That means books such as Unger's Cut-elimination, Normalization, and the Theory of Proofs, Troelstra's Lectures on Linear Logic, Aczel's Non-well-founded Sets, van Benthem's Manual of Intensional Logic, and Goldblatt's Logics of Time and Computation are now available online and for free. (HT: Shawn)

Also of interest here will be McCarthy's Defending AI research, and Modal logic and process algebra : a bisimulation perspective, edited by Venema, de Rijke and Ponse.

Generative Code Specialisation for High-Performance Monte Carlo Simulations (Don Stewart, Hugh Chaffey-Millar, Gabriele Keller, Manuel M. T. Chakravarty and Christopher Barner-Kowollik) is a nice example of exploiting PL theory techniques (relevant keywords highlighted below) to combine a need for generality with high performance, to achieve outstanding results:

We address the tension between software generality and performance in the domain of scientific and financial simulations based on Monte-Carlo methods. To this end, we present a novel software architecture, centred around the concept of a specialising simulator generator, that combines and extends methods from generative programming, partial evaluation, runtime code generation, and dynamic code loading. The core tenet is that, given a fixed simulator configuration, a generator in a functional language can produce low-level code that is more highly optimised than a manually implemented generic simulator. We also introduce a skeleton, or template, capturing a wide range of Monte-Carlo methods and use it to explain how to design specialising simulator generators and how to generate parallelised simulators for multi-core and distributed-memory multiprocessors.

We evaluated the practical benefits and limitations of our approach by applying it to a highly relevant problem in computational chemistry. More precisely, we used a Markov-chain Monte-Carlo method for the study of advanced forms of polymerisation kinetics. The resulting implementation executes faster than all competing software products, while at the same time also being more general. The generative architecture allows us to cover a wider range of chemical reactions and to target a wider range of high-performance architectures (such as PC clusters and SMP multiprocessors).

We show that it is possible to outperform low-level languages with functional programming in domains with very stringent performance requirements if the domain also demands generality.

The project web site provides the Haskell and C source. The Haskell code generates specialized C code for specific simulations, which is then compiled and dynamically loaded.