Lambda the Ultimate

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...

Oleg has an interesting piece that I haven't found mentioned on LtU (though it dates from 2000):

Blending static and dynamic typing: Scheme programming in ML

We show several examples of writing ML (OCaml) code in the style of Scheme programs, taking the fullest advantage of latent typing and placing no type annotations. The ML code features:

• intentionally polymorphic functions: Scheme display
• lists of variously intentionally typed elements
• functions with a variable number of polymorphic arguments: *
• self-application combinator
• higher-order polyvariadic intensionally polymorphic function: Scheme for-each

[...]

The code is trivial -- and that is the point. Defining and using the Universal type in a statically typed language is indeed embarrassingly easy. The code has not a single type annotation, and looks as dynamically typed as Scheme code. The source language is still OCaml, with static typing present and available to the programmer. Thus ML offers a blend of dynamic and static type programming; it's a programmer who chooses the proportions of this blend.

(disclaimer: I'm not posting this to start another religious battle, but as an interesting example)

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.