Lambda the Ultimate

From the press release:

The first of the three steps of the ISO standardization process has been successfully completed. The Working Group in charge of the technical details of the standard, named WG 9 and headed by the convener Mr. James Moore, unanimously approved the Ada 2005 standard on May 1st, 2006.

The press release includes a brief summary of the new features in the new version of the Ada language. Some of these features were mentioned here before.

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy has written Formal verification of a C-Compiler frontend. Some previous work is already mentioned on LtU here. Abstract:

This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the speci- fication language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.

ML Modules and Haskell Type Classes: A Constructive Comparison
Stefan Wehr and Manuel M.T. Chakravarty

Researchers repeatedly observed that the module system of ML and the type class mechanism of Haskell are related. So far, this relationship has not been formally investigated. The work at hand fills this gap by presenting a constructive comparison between ML modules and Haskell type classes; that is, it introduces two formal translations from modules to type classes and vice versa, which enable a thorough comparison of the two concepts.

And the conclusions...

In this work, we demonstrated how ML modules can be translated to Haskell type classes, proved that the translation preserves type correctness, and provided an implementation of the translation. The source language of the translation is a sub-set of Standard ML, the most important feature missing is the ability to define nested structures. The target language is a subset of Haskell 98 extended with multi-parameter type classes and (abstract) associated type synonyms. Abstract associated type synonyms, another contribution of this work, are used to translate abstract types to Haskell. Our practical experience suggests that it is feasible to use the general idea behind the translation for practical programming because some of the overhead introduced by the formal translation is avoided when writing the
Haskell code by hand.

Furthermore, we showed that Haskell type classes can be translated into ML modules by using first-class structures as runtime evidence for type class constraints. We proved that this translation also preserves type correctness and implemented it. The source language of the translation is a subset of Haskell 98, which does not support constructor classes, class methods with constraints, and default definitions for methods. The target language is a subset of Standard ML extended with first-class structures and recursive functors. It is not recommended writing programs in the style of the translation by hand because too much syntactic overhead is introduced by explicit dictionary abstraction and application. However, the translation provides a good starting point for integrating type classes into the ML module system.

Finally, we presented a thorough comparison between ML modules and Haskell type classes, which fills a serious gap in the literature because it is the first comparison between the two concepts that is based on formal translations. The comparison shows that there are also significant differences between modules and type classes.

Recently found a paper rebuking the Church-Turing thesis on the grounds of infinite computations and the Y-combinator. It's a tongue-in-cheek poke at Turing's UTM vs McCarthy's LISP, but has some interesting ideas in it. I know the researcher, he's a good guy and should join LtU if he's not lurking already. Although you may question his sanity after reating this..

Infinite Order Logic and the Church-Turing Thesis
Dimitris Vyzovitis

His conclusions include:

• LISP is an infinite-order logic
• Halting problem is decidable in LISP (modulo Y-combinators)
• P = NP in LISP

You can see his research and other papers (under resume) here.