Lambda the Ultimate

Many loops in probabilistic inference map almost every individual in their domain to the same result. Running such loops symbolically takes time sublinear in the domain size. Using normalization by evaluation with first-class delimited continuations, we lift inference procedures to reap this speed-up without interpretive overhead. To express nested loops, we use multiple control delimiters for metacircular interpretation. To express loops over a powerset domain, we convert nested loops over a subset to unnested loops.

The paper is a bit hard to follow, but there are enough little tricks here to merit attentive reading. Or better yet, read the code. The basic PLT idea might be summed as doing abstract interpretation on a shallowly embedded DSL using delimited continuations.

A Verified Compiler for an Impure Functional Language

We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to big-step operational semantics for the source and target languages. Compilation is staged and includes standard phases like translation to continuation-passing style and closure conversion, as well as a common subexpression elimination optimization. In this work, our focus has been on discovering and using techniques that make our proofs easy to engineer and maintain. While most programming language work with proof assistants uses very manual proof styles, all of our proofs are implemented as adaptive programs in Coq’s tactic language, making it possible to reuse proofs unchanged as new language features are added.

In this paper, we focus especially on phases of compilation that rearrange the structure of syntax with nested variable binders. That aspect has been a key challenge area in past compiler verification projects, with much more effort expended in the statement and proof of binder-related lemmas than is found in standard pencil-and-paper proofs. We show how to exploit the representation technique of parametric higher-order abstract syntax to avoid the need to prove any of the usual lemmas about binder manipulation, often leading to proofs that are actually shorter than their pencil-and-paper analogues. Our strategy is based on a new approach to encoding operational semantics which delegates all concerns about substitution to the meta language, without using features incompatible with general-purpose type theories like Coq’s logic.

The latest from Adam Chlipala. Yet another evolutionary step for Lambda Tamer. Between this and Ynot the Coq/certified compiler story seems to be getting more impressive nearly daily.

Certified Web Services in Ynot

In this paper we demonstrate that it is possible to implement certified web systems in a way not much different from writing Standard ML or Haskell code, including use of imperative features like pointers, files, and socket I/O. We present a web-based course gradebook application developed with Ynot, a Coq library for certified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot’s underlying Hoare logic with event traces to reason about I/O behavior. Expressive abstractions allow the modular certification of both high level specifications like privacy guarantees and low level properties like memory safety and correct parsing.

Ynot, always ambitious, takes another serious swing: extracting a real web application from a proof development. In some respects the big news here is the additional coverage that Ynot now offers in terms of support for file and socket I/O, and the event trace mechanism. But there's even bigger news, IMHO, which is the subject of another paper that warrants a separate post.

In a Qilang mailing list email Marker Tarver, creator of Qi, says

In a month I will be packing to go to India; this time for an extended
period. But its also a goodbye to Qi and computing. At some point
you have to acknowledge that Qi doesn't pay its way. It was fun
though and I'm not sad about it.

Qi has been a journey that began nearly 20 years ago when I was a very
different person and worked for a university. But the book on Qi II
marks a natural watershed. I need to move on. By September I will be
gone.

Robert Hieb, R. Kent Dybvig, and Carl Bruggeman. Representing Control in the Presence of First-Class Continuations. ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, June 1990.

Languages such as Scheme and Smalltalk that provide continuations as first-class data objects present a challenge to efficient implementation. Allocating activation records in a heap has proven unsatisfactory because of increased frame linkage costs, increased garbage collection overhead, and decreased locality of reference. However, simply allocating activation records on a stack and copying them when a continuation is created results in unbounded copying overhead. This paper describes a new approach based on stack allocation that does not require the stack to be copied when a continuation is created and that allows us to place a small upper bound on the amount copied when a continuation is reinstated. This new approach is faster than the naive stack allocation approach, and it does not suffer from the problems associated with unbounded copying. For continuation-intensive programs, our approach is at worst a constant factor slower than the heap allocation approach, and for typical programs, it is significantly faster. An important additional benefit is that recovery from stack overflow is handled gracefully and efficiently.

Many Scheme implementations do not implement call/cc particularly well, but it is important to remember that call/cc is not inherently slow. This is the classic paper describing a clever run-time representation that supports call/cc efficiently.

Simon Marlow:

...with ICFP and the Haskell Symposium approaching we felt it was time to
get the new process moving and hopefully produce a language revision...

In the coming weeks we'll be refining proposals in preparation for
Haskell 2010. By all means suggest more possibilities; however note
that as per the new process, a proposal must be "complete" (i.e. in the
form of an addendum) in order to be a candidate for acceptance.

More here.

Lambda calculus as animated alligators and eggs. Virtually guaranteed to turn any 4 year old into a PLT geek.

The non-animated game was mentioned previously on LTU here.

The Functional Payout Framework (fpf) is a Haskell application that uses an embedded domain-specific functional language to represent and process exotic financial derivatives. Whereas scripting languages for pricing exotic derivatives are common in banking, fpf uses multiple interpretations to not only price such trades, but also to analyse the scripts to provide lifecycle support and more. This paper discusses fpf in relation to the wider trading workflow and our experiences in using a functional language in such a system as both an implementation language and a domain-specific language.

Section 3 is a nice discussion of why Haskell was chosen. Section 4 illustrates one of the major benefits of using DSLs, namely that different backends can be applied to programs written in the DSL, allowing various types of runtime behavior and analysis without the need to re-code each program for each purpose (thus n+m, rather than n*m programs).

Another topic that may be worth discussing is the authors' dislike of point free style.

What we really need, of course, are DSLs for financial regulation (and possibly for specifying various definitions of honesty), but that's a separate issue...

If optimization and intermediate languages for lazy functional languages are your things, take a look at Types are Calling Conventions by Max Bolingbroke and Simon Peyton Jones.

It is common for compilers to derive the calling convention of a function from its type. Doing so is simple and modular but misses many optimisation opportunities, particularly in lazy, higher-order functional languages with extensive use of currying. We restore the lost opportunities by defining Strict Core, a new intermediate language whose type system makes the missing distinctions: laziness is explicit, and functions take multiple arguments and return multiple results.

Polymorphic Delimited Contiunations by Kenichi Asai and Yukiyoshi Kameyama, in the 5^th ASIAN Symposium on Programming Languages and Systems (2007).

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.

Now, the real reason that I post this is because of Oleg's ShiftResetGenuine, which implements polymorphic delimited continuations in Haskell, and primarily cites this paper as well as Robert Atkey's Parameterized Notions of Computation. So if you find this paper challenging to read, Oleg provides you with a concrete playground in which to experiment.

It's also notable that Matthieu Sozeau has GenuineShiftReset available, which is a Coq version of Oleg's code.