Lambda the Ultimate

Proving the Correctness of Reactive Systems Using Sized Types, John Hughes, Lars Pareto, Amr Sabry. 1996.

We have designed and implemented a type-based analysis
for proving some basic properties of reactive systems. The
analysis manipulates rich type expressions that contain information
about the sizes of recursively defined data structures.
Sized types are useful for detecting deadlocks, nontermination,
and other errors in embedded programs. To
establish the soundness of the analysis we have developed
an appropriate semantic model of sized types.

Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming, John Hughes, Lars Pareto. 1999.

We present a functional language with a type system such that well
typed programs run within stated space-bounds. The language is a
strict, first-order variant of ML with constructs for explicit
storage management. The type system is a variant of Tofte and
Talpin's region inference system to which the notion of sized types,
of Hughes, Pareto and Sabry, has been added.

Continuing the series on total functions and termination, a couple of papers co-authored by someone who can tell you why functional programming matters. The first paper introduces a type system that uses sized types to track termination, productivity and liveness properties for algebraic and coalgebraic data. The second papers extends the system to track memory regions and other space effects.

Previously mentioned on LtU quite a few times, but only on comments.

Business Objects' Quark Framework for Java, which includes a Haskell-like language CAL has recently been released as open source under a BSD style license. Details and downloads are available on the Main Business Objects Labs Page for CAL. The framework, with or without sources, can be downloaded without any kind of registration.

For those who did not see last year's announcements and the seeding of the framework (without sources), there are a number of documents available that should help with understanding the nature of the CAL language, the SDK and tools.

Naturally, we hope that people will provide feedback and contribute in other ways, and we have a discussion forum available for this purpose - see link on the main page.

We continue to be very active on this project, with a current focus on improving the Eclipse integration as well as continued evolution of the language.

Luke Evans
Chief Scientist, VP Research, Business Objects

[I think I got onto this via some LtU comment that I can't find now.] Looks like MML has been given real legs via a compiler in Haskell. Per chance, has anybody used this? Now if only there were a debugger, and good concurrency support...