Lambda the Ultimate

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.

Dao (posted here before) was not initially designed to be a functional programming language, but with time some functional features were added to the language. And recently I designed and implemented (for the next release) several built-in methods to increase its support for functional style programming.

These methods are documented here: http://www.daovm.net/space/dao/thread/137. It is slightly similar to that of Ruby with a few distinctive feature. Basically, it looks like something like this,

RESULT = METHOD( PARAMETER ) -> |VARIABLE| { EXPRESSION }

Here PARAMETER can be one or more list or array (almost all these methods are applicable to numeric arrays), or other data types depending on METHOD. |VARIABLE| is to declare variables associated with list/array items or indices etc. |VARIABLE| can also be omitted so that default parameter names will be used.

EXPRESSION is the inlined function to be applied, normal statements (except return statement) can also be used, in this case, the statement code block must be separated from the EXPRESSION by "return" key word. EXPRESSION can actually be multiple expressions separated by comma(s) in method such as map(), which will return a list of tuples in such cases.

Function composition is simply supported by allowing one or more ->|...|{...} constructs to append one after another. In such cases, |VARIABLE| can be used to declare variables referring the results of EXPRESSION in the previous ->|...|{...} construct.

A simple example:

a = { 1, 2, 3 }
b = { 7, 8, 9 }

zip_ab = map( a, b ) -> |u,v| { u, v }
zip_ab = map( a, b ) -> { x, y }
zip_ab = select( a, b ) -> { 1 }

c = map( a, b ) -> |x,y| { x-y, x+y } -> |u,v| { u*v }

d = map( a ) -> |x| {
  u = 10*x;
  v = x+10;
  if( u < v ) u += v;
  return u*v 
}

e = unfold( 5 ) -> |x| { while x > 0 return x - 1 }

e = unfold( 5 ) -> |x| {
  stdio.println(x)
  while x > 0 return x - 1
}

Your comments, suggestions or opinions are welcome,
I think they will be very invaluable for the future improvements. Many thanks in advance!

I'm part of a group that is writing a paper trying to explain, to other computer scientists and engineers, the importance to universities of teaching undergraduate courses on programming languages. (The group is a subcommittee of the (newly formed) ACM SIGPLAN education board.) The hope is that this paper will be useful in influencing the IEEE/ACM curriculum revisions and ABET accreditation process. It might also help motivate students in such a course.

So, we are seeking a set of examples (or data) that say how the kind of knowledge taught in (esp. undergraduate) courses on programming languages help students in their careers. These careers could be in industry or research, but probably the most interesting and least debatable examples would come from industry. What we'd like are examples that would be convincing to computer scientists and engineers who are outside the field of programming languages, since those are the ones we have to sell on the importance of courses in programming languages.

An example of such an example is Paul Graham's paper "Beating the Averages" (see http://www.paulgraham.com/avg.html). Other examples we know something about, but would like more details about, are LexiFi's use of abstraction ideas in financial contracts ("Composing Contracts: An Adventure in Financial Engineering", by Simon Peyton Jones, Jean-Marc Eber, and Jullian Seward, in IFIP 2000), Ericsson's use of Erlang (http://erlang.org/doc.html), Twitter's use of Scala ( http://www.artima.com/scalazine/articles/twitter_on_scala.html), software transactional memory and Haskell ( http://www.haskell.org/haskellwiki/Software_transactional_memory).

If you know of more examples, please let us know by replying to this thread, preferably with a reference or link. Since the functional programming community has done an especially good job of making clear what their commercial successes are (see http://cufp.galois.com/), we are particularly interested in ideas from the programming language community that are not just "apply functional programming ideas" (although those are welcome too), for example older stories of how using OO gave a market advantage, or how some company used logic programming to configure computers. The best kind of examples would relate directly to topics typical of undergraduate programming languages courses (e.g., "How I made a million dollars by using static scoping" :-).

Hoopl: Dataflow Optimization Made Simple by Norman Ramsey, João Dias, and Simon Peyton Jones.

We present Hoopl, a Haskell library that makes it easy for compiler writers to implement program transformations based on dataflow analyses. The compiler writer must identify (a) logical assertions on which the transformation will be based; (b) a representation of such assertions, which should form a lattice of finite height; (c) transfer functions that approximate weakest preconditions or strongest postconditions over the assertions; and (d) rewrite functions whose soundness is justified by the assertions. Hoopl uses the algorithm of Lerner, Grove, and Chambers (2002), which can compose very simple analyses and transformations in a way that achieves the same precision as complex, handwritten ``super-analyses.'' Hoopl will be the workhorse of a new back end for the Glasgow Haskell Compiler (version 6.12, forthcoming).

A continuation of work previously mentioned on LtU here. Original people, new language. More purity, more goodness. Sinfully, there does not yet seem to be a hackage package.