Lambda the Ultimate

Juan Chen. A Typed Intermediate Language for Compiling Multiple Inheritance.

This paper presents a typed intermediate language EMI that supports multiple and virtual inheritance of classes in C++-like languages. EMI faithfully represents standard implementation strategies of object layout, "this" pointer adjustment, and dynamic dispatch. The type system is sound. Type checking is decidable. The translation from a source language to EMI preserves types. We believe that EMI is the first typed intermediate language that is expressive enough for describing implementation details of multiple and virtual inheritance of classes.

If you really must have mutiple inheritance...

During the week of Nov. 7, I will be touring the US to visit universities and other institutions teaching with my book (CTM) or thinking of teaching with it. For those who have not seen the book, it teaches programming in a way that is both broad and deep. It covers both practice (writing and running programs) and theory (semantics and reasoning about programs), and covers most of the important programming paradigms in a simple and uniform way. It is based on a long-term research collaboration (more than 15 years by now) by many people on understanding programming languages and their underlying concepts.

I will be giving talks and also talking with people. I can answer any questions about the book, its motivation and background, and our teaching experience. I can also offer advice on how to fit the book or its approach in your computer science curriculum.

I am now starting to plan the tour. If you are in the US and you would like me to visit your institution, please send me email (pvr@info.ucl.ac.be).

Believe it or not, Lambda the Ultimate is five years old! Wow.

If someone would have told me five years ago that LtU will be around that long, I'd call him crazy. I still remember trying to recruit new members and trying to spread the word. Today? The number of members increases daily, whether I like it or not...

It's gratifying to see that many of the original members are still active, and that many members have their own specific roles in our virtual community. It's great to see people's interests and voice evolve over time, as well as to welcome guests and more occasional visitors.

Since moving to the new site (thanks Anton!) the membership and readership have increased dramatically. A rapid increase of this kind can undermine the norms and culture of a community, but I think we are doing fine, thanks mainly to the tone set by the LtU regulars. From time to time we may slip and the tone gets a little harsh, but what can you expect when static typing is being discussed? Overall, I think we are handling the growth remarkably well, and the new members make the dicussion more interesting and diverse.

The discussion group has become much more active than it was in the past, due to the increased readership. This is a good thing, of course, but I hope the blog can keep up. Being extremely busy prevents me to contribute new stories as often as I want, but I was glad to see how many volunteered to become editors. Now all they have to do is start posting more often..

Thanks again, guys. LtU keeps surprising and informing me, and frankly, what more can you ask for?

It's been a while since the last LtU link to Vijay Saraswat papers.

Concurrent Clustered Programming

We present the concurrency and distribution primitives of X10, a modern, statically typed, class-based object-oriented (OO) programming language, designed for high productivity programming of scalable applications on high-end machines. The basic move in the X10 programming model is to reify locality through a notion of place, which hosts multiple data items and activities that operate on them. Aggregate objects (such as arrays) may be distributed across multiple places. Activities may dynamically spawn new activities in mulitple places and sequence them through a finish operation that detects termination of activities. Atomicity is obtained through the use of atomic blocks. Activities may repeatedly detect quiescence of a data-dependent collection of (distributed) activities through a notion of clocks, generalizing barriers. Thus X10 has a handful of orthogonal constructs for space, time, sequencing and atomicity. X10 smoothly combines and generalizes the current dominant paradigms for shared memory computing and message passing. We present a bisimulation-based operational semantics for X10 building on the formal semantics for "Middleweight Java''. We establish the central theorem of X10: programs without conditional atomic blocks do not deadlock.

To appear in the Proceedings of CONCUR, August 2005.

---

[on edit: added missing link, sorry]

... or how is the title of this paper pronounced?

We make the notion of scope in the lambda-calculus explicit. To that end, the syntax of the lambda-calculus is extended with an end-of-scope operator [adbmal], matching the usual opening of a scope due to lambda. Accordingly, beta-reduction is extended to the set of scoped lambda-terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped beta-reduction. Confluence of beta-reduction for the ordinary lambda-calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, alpha-equivalence is needed. All our proofs have been verified in Coq.

While playing with my own lambda-machine (derivative of CEK in Java) I decided that I would like to control scope better - so I found this paper.

See also Lambdascope previously mentioned on LtU.

Buffer overflows are one problem that the world seems to know how to solve, as evidenced by languages such as Java, C#, and Python that are not susceptible to the issue. On the surface, the reason why we still are plagued by the problem is obvious: we still use C, C++, and assembly in a heck of a lot of applications.

Among the things mentioned in this essay: String-handling libraries, Static analysis tools, Cyclone, and zero knowledge protocols.

What happened to all the editors? Is everyone on vaction? ;-)

On the Revival of Dynamic Languages pdf

The programming languages of today are stuck in a deep rut that has developed over the past 50 years... We argue the need for a new class of dynamic languages... features such as dynamic first-class namespaces, explicit meta-models, optional, pluggable type systems, and incremental compilation of running software systems.

A couple of weeks ago, I posed the following in my blog: what are the grand challenges of software and software engineering? What do we know we don't know?

I had about a dozen people rise to the question and a lively discussion among many of them unfolded via email. Following are some highlights of that correspondence.

Even though most of the responses weren't about coding and programming language issues, I think this discussion is worth a look.

It might be intereting to discuss if and to what extent programming languages can help improve the state of the art in SE.

I'll go first and argue that a large part of the answer to How to keep significantly raising the level of abstraction in face of ever growing software complexity? lies in better programming languages. Especially as regards module systems, expressive type systems and better concurrency and distributed computing idioms.

A Concurrent Lambda Calculus with Futures

We introduce a new concurrent lambda calculus with futures, lambda(fut), to model the operational semantics of Alice, a concurrent extension of ML. lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that yields the full expressiveness to define, combine, and implement a variety of standard concurrency constructs such as channels, semaphores, and ports. We present a linear type system for lambda(fut) by which the safety of such definitions and their combinations can be proved: Well-typed implementations cannot be corrupted in any well-typed context.

To all the fans of Mozart and especially Stockhausen :-)

Abstract interpretation for constraint handling rules. Tom Schrijvers, Peter J. Stuckey, Gregory J. Duck. PPDP’05

Program analysis is essential for the optimized compilation of Constraint Handling Rules (CHRs) as well as the inference of behavioral properties such as confluence and termination. Up to now all program analyses for CHRs have been developed in an ad hoc fashion.In this work we bring the general program analysis methodology of abstract interpretation to CHRs: we formulate an abstract interpretation framework over the call-based operational semantics of CHRs. The abstract interpretation framework is non-obvious since it needs to handle the highly non-deterministic execution of CHRs. The use of the framework is illustrated with two instantiations: the CHR-specific late storage analysis and the more generally known groundness analysis. In addition, we discuss optimizations based on these analyses and present experimental results.

I haven't read this paper carefully yet, but since the authors claim it is the first published account of abstract interpretation for CHRs, I decided to mention it here anyway.