Lambda the Ultimate

On Decidability of Nominal Subtyping with Variance. Andrew J. Kennedy, Benjamin C. Pierce. FOOL'07. January 2007

We investigate the algorithmics of subtyping in the presence of nominal inheritance and variance for generic types, as found in Java 5, Scala 2.0, and the .NET 2.0 Intermediate Language. We prove that the general problem is undecidable and characterize three different decidable fragments. From the latter, we conjecture that undecidability critically depends on the combination of three features that are not found together in any of these languages: contravariant type constructors, class hierarchies in which the set of types reachable from a given type by inheritance and decomposition is not always finite, and class hierarchies in which a type may have multiple supertypes with the same head constructor. These results settle one case of practical interest: subtyping between ground types in the .NET intermediate language is decidable; we conjecture that our proof can also be extended to show full decidability of subtyping in .NET. For Java and Scala, the decidability questions remain open; however, the proofs of our preliminary results introduce a number of novel techniques that we hope may be useful in further attacks on these questions.

The undecidability of subtyping is proved by reduction from the Post Correspondence Problem. Section 5 presents several decidable fragments.

Hot stuff!

Meta-Compilation of Language Abstractions, a dissertation by Pinku Surana.

High-level programming languages are currently transformed into efficient low-level code using optimizations that are encoded directly into the compiler. Libraries, which are semantically rich user-level abstractions, are largely ignored by the compiler. Consequently, library writers often provide a complex, low-level interface to which programmers "manually compile" their high-level ideas. If library writers provide a high-level interface, it generally comes at the cost of performance. Ideally, library writers should provide a high-level interface and a means to compile it efficiently.

This dissertation demonstrates that a compiler can be dynamically extended to support user-level abstractions. The Sausage meta-compilation system is an extensible source-to-source compiler for a subset of the Scheme programming language. Since the source language lacks nearly all the abstractions found in popular languages, new abstractions are implemented by a library and a compiler extension. In fact, Sausage implements all its general-purpose optimizations for functional languages as compiler extensions. A meta-compiler, therefore, is merely a shell that coordinates the execution of many external extensions to compile a single module. Sausage demonstrates that a compiler designed to be extended can evolve and adapt to new domains without a loss of efficiency.

A very interesting and detailed paper, which touches on many perennial LtU subjects, and once again shifts the line between user programs and the compiler. If you're tempted to say "this sounds like X...", then read Chapter 2, which gives a comprehensive comparison to alternative approaches, including static type inference, traditional macro systems, templates, partial evaluation, and multi-stage languages such as MetaML and MetaOCaml.

Some carefully selected quotes which I think summarize the summary quite well:

The Sausage system provides a framework for programmers to write new domain-specific optimizations and inject them into the main compiler.
...
This dissertation takes the rather extreme view that anything beyond Core Scheme is a compiler extension.

Pinku Surana will be presenting this work at a meeting of LispNYC on Feb 13th in New York City. An announcement with details of the meeting can be found here.

I am sad to note that Jean Ichbiah, the lead designer of Ada, passed away on January 26, 2007.

Ada83, the reference manual for which appeared in 1983, is commonly known as the first version of Ada. Prior to that, in 1977, four contractors were picked to produce prototype languages, matching the requirements of the Ironman document (which led the way to the final Ada requirements specification, the Steelman). The prototypes were named green, red, blue and yellow. The green language, proposed by a team at Cii Honeywell Bull led by Jean D. Ichbiah, was chosen and led the way to Ada83. See here for more detailed timeline of the history of Ada.

While the design of Ada83 and Ada95 were both team efforts, in both cases the design was guided by a team leader whose vision and aesthetics regarding programming languages shaped the language. All versions of Ada owe much to Jean Ichbiah who shaped the core of the language used today.

Proposal to NSF – Granted on August 31st 2006 (pdf)

This opens the exciting possibility of creating a practical working system that is also its own model – a whole system from the end-users to the metal that could be extremely compact (we think under 20,000 lines of code) yet practical enough to serve both as a highly useful end-user system and a “system to learn about systems”. I.e. the system could be compact, comprehensive, clear, high-level, and understandable enough to
be an “Exploratorium of itself”. It would:
...
- Create a test-bed environment for experiments into “the programming of the future” for end-users and pros

Separation Logic: A Logic for Shared Mutable Data Structure, John C. Reynolds. LICS 2002

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

I think this paper has been mentioned several times in discussion on LtU, but never gotten an article of its own. It's a really elegant piece of work that addresses the biggest weakness of Hoare logic: that you cannot do local, modular correctness proofs of programs that use aliasable state.

(I should say my own research is on using separation logic in languages like ML or Haskell, so I am a partisan!)