Lambda the Ultimate

Towards a Mechanized Metatheory of Standard ML, Daniel K. Lee, Karl Crary, and Robert Harper.

We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest.

The way that most programming languages end up working is by defining a smaller core language to which the constructions in the base language are translated. This means that you can prove the type-safety of a programming language by showing that the internal language is type safe, and that every type-correct program in the full language translates to a type-correct expression in the internal language. In this paper, the authors carried out the mechanization of a core language for SML. The next step is mechanizing the correctness of an elaborator from SML to this core language, and then full, no-foolin' SML will have a fully machine-checked correctness proof.

A March 27, 2007 draft of a paper by Conal Elliot:

We present a user-friendly approach to unifying program creation and execution, based on a notion of “tangible values” (TVs), which are visual and interactive manifestations of pure values. Programming happens by gestural composition of TVs. Our goal is to give end-users the ability to create parameterized, composable content without imposing the usual abstract and linguistic working style of programmers. We hope that such a system will put the essence of programming into the hands of many more people, and in particular people with artistic/visual creative style.

In realizing this vision, we develop algebras for visual presentation and for “deep” function application, where function and argument may both be nested within a structure of tuples, functions, etc. Composition gestures are translated into chains of combinators that act simultaneously on statically typed values and their visualizations.

A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language

I present a certified compiler from simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. I demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge automatically large parts of the proof obligations.

Software/proof source code and documentation

Slides are available from a talk I gave at the Projet Gallium seminar at INRIA Rocquencourt, in OpenOffice and PDF formats.

I found this while attempting to follow up on this post. The approach taken here—dependently-typed ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proof-carrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive big-step operational semantics, also done in Coq. Fascinating stuff.

Concoqtion: Indexed Types Now!

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate F_ω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading
proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

The follow-up to Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference, discussed earlier. Good stuff.

Update: There's now a public Concoqtion web site!

Josh, does this answer your question? :-)

Static Typing for a Faulty Lambda Calculus. David Walker. Lester Mackey. Jay Ligatti, George A. Reis, and David I. August.

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While the likelihood that such transient faults will cause any significant damage may seem remote, over the last several years transient faults have caused costly failures in high-end machines at America Online, eBay, and the Los Alamos Neutron Science Center, among others. Because susceptibility to transient faults is proportional to the size and density of transistors, the problem of transient faults will become increasingly important in the coming decades.

This paper defines the first formal, type-theoretic framework for studying reliable computation in the presence of transient faults. More specifically, it defines lambda-zap, a lambda calculus that exhibits intermittent data faults. In order to detect and recover from these faults, lambda-zap programs replicate intermediate computations and use majority voting, thereby modeling software-based fault tolerance techniques studied extensively, but informally.

To ensure that programs maintain the proper invariants and use lambda-zap primitives correctly, the paper defines a type system for the language. This type system guarantees that well-typed programs can tolerate any single data fault. To demonstrate that lambda-zap can serve as an idealized typed intermediate language, we define a type-preserving translation from a standard simply-typed lambda calculus into lambda-zap.

Lightweight static resources: Sexy types for embedded and systems programming. Oleg Kiselyov and Chung-chieh Shan.

It is an established trend to develop low-level code—embedded software, device drivers, and operating systems—using high-level languages, especially the advanced abstraction facilities in functional programming. To be reliable and secure, low-level
code must correctly manage space, time, and other resources, so special type systems and verification tools arose to regulate resource access statically. However, a general-purpose functional programming language practical today can provide the same static assurances, also with no run-time overhead. We substantiate this claim and promote the trend with two security kernels in the domain of device drivers:
1. one built around raw pointers, to track and arbitrate the size, alignment, write permission, and other properties of memory areas across indexing and casting;
2. the other built around a device register, to enforce protocol and timing requirements while reading from the register.
Our style is convenient in Haskell thanks to custom kinds and predicates (as type classes); type-level numbers, functions, and records (using functional dependencies); and mixed type- and term-level programming (enabling partial type signatures).

The related source code is also available.

Ken and Oleg's work is always worth checking out, so I urge LtU readers to go and see the solutions they propose aimed at allowing programmers of low level system software to work with raw pointers, device registers etc., while statically enforcing invariants such as pointer validity and in-bounds memory access.

The link is to a near final draft of a paper to be presented at TFP2007, and comments - I'm told - will be appreciated, especially as regards the "Related Work" section. Be quick with your comments, though, since the "camera ready" date is tomorrow...

The Design and Implementation of a Dataflow Language for Scriptable Debugging, Guillaume Marceau, Gregory H. Cooper, Jonathan P. Spiro, Shriram Krishnamurthi, and Steven P. Reiss.

Debugging is a laborious, manual activity that often involves the repetition of common operations. Ideally, users should be able to describe these repetitious operations as little programs. Debuggers should therefore be programmable, or scriptable. The operating environment of these scripts, however, imposes interesting design challenges on the programming language in which these scripts are written.

This paper presents our design of a language for scripting debuggers. The language offers powerful primitives that can precisely and concisely capture many important debugging and comprehension metaphors. The paper also describes a pair of debuggers, one for Java and the other for Scheme, built in accordance with these principles. The paper includes concrete examples of applying this debugger to programs.

We've seen a paper on compiling dataflow languages, so here's one on an interesting application.

Lowering: A Static Optimization Technique for Transparent Functional Reactivity, Kimberley Burchett, Gregory H. Cooper, and Shriram Krishnamurthi. PEPM 2007.

Functional Reactive Programming (FRP) extends traditional functional programming with dataflow evaluation, making it possible to write interactive programs in a declarative style. An FRP language creates a dynamic graph of data dependencies and reacts to changes by propagating updates through the graph. In a transparent FRP language, the primitive operators are implicitly lifted, so they construct graph nodes when they are applied to time-varying values. This model has some attractive properties, but it tends to produce a large graph that is costly to maintain. In this paper, we develop a transformation we call lowering, which improves performance by reducing the size of the graph. We present a static analysis that guides the sound application of this optimization, and we present benchmark results that demonstrate dramatic improvements in both speed and memory usage for real programs.

Whenever I read about compiler optimizations, I try (with mixed success) to relate them to transformations in the lambda calculus. I haven't managed to figure out what's going on with the dip construct the authors propose, but I would guess that the place to look is the proof theory of the necessity operator in modal logic -- dataflow programming can be seen as a kind of stream programming, and streams form a comonad over the lambda calculus, and comonads give semantics to the modal necessity (box) operator.

Lightweight Fusion by Fixed Point Promotion, Atsushi Ohori and Isao Sasano.

This paper proposes a lightweight fusion method for general recursive function definitions. Compared with existing proposals, our method has several significant practical features: it works for general recursive functions on general algebraic data types; it does not produce extra runtime overhead (except for possible code size increase due to the success of fusion); and it is readily incorporated in standard inlining optimization. This is achieved by extending the ordinary inlining process with a new fusion law that transforms a term of the form f o (fix g.λx.E) to a new fixed point term fix h.λx.E' by promoting the function f through the fixed point operator.

This is a sound syntactic transformation rule that is not sensitive to the types of f and g. This property makes our method applicable to wide range of functions including those with multi-parameters in both curried and uncurried forms. Although this method does not guarantee any form of completeness, it fuses typical examples discussed in the literature and others that involve accumulating parameters, either in the foldl-like specific forms or in general recursive forms, without any additional machinery.

In order to substantiate our claim, we have implemented our method in a compiler. Although it is preliminary, it demonstrates practical feasibility of this method.

Deforestation is one of those optimizations every functional programmer who has ever had to rewrite a beautiful composition of maps and filters into an evil, ugly explicit fold has always longed for. Unfortunately, the standard lightweight fusion algorithms have trouble with examples as simple as foldl, and this paper has a very nice account of a simple algorithm that can handle it.

The Missing Link - Dynamic Components for ML, Andreas Rossberg. ICFP 2006.

Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive first-class component system for ML. It provides dynamic linking in a type-safe and type-flexible manner, and allows selective execution in sandboxes. The system is defined solely by reduction to higher-order modules plus an extension with simple module-level dynamics, which we call packages. To represent components outside processes we employ generic pickling. We give a module calculus formalising the semantics of packages and pickling.

This is a very nice paper showing how to integrate dynamic loading into the ML module system. Er, I guess I'm repeating the abstract. I thought this paper, in addition to the feature it gave, was also a good demonstration of how to put the Dreyer-Crary-Harper account of ML modules to work.