Concurrent Revisions is a Microsoft Research project doing interesting work in making concurrent programming scalable and easier to reason about. These papers work have been mentioned a number of times here on LtU, but none of them seem to have been officially posted as stories.
Concurrent Revisions are a distributed version control-like abstraction  for concurrently mutable state that requires clients to specify merge functions that make fork-join deterministic, and so make concurrent programs inherently composable. The library provide default merge behaviour for various familiar objects like numbers and lists, and it seems somewhat straightforward to provide a merge function for many other object types.
They've also extended the work to seamlessly integrate incremental and parallel computation  in a fairly intuitive fashion, in my opinion.
Their latest work  extends these concurrent revisions to distributed scenarios with disconnected operations, which operate much like distributed version control works with source code, with guarantees of eventual consistency.
All in all, a very promising approach, and deserving of wider coverage.
 Sebastian Burckhardt and Daan Leijen, Semantics of Concurrent Revisions, in European Symposium on Programming (ESOP'11), Springer Verlag, Saarbrucken, Germany, March 2011
Feature-Oriented Programming with Object Algebras, by Bruno C.d.S. Oliveira, Tijs van der Storm, Alex Loh, William R. Cook:
A follow-up to Object Algebras, this new paper addresses a few of the limitations described in that LtU thread by adding type constructor polymorphism to increase their safety. The paper describes an implementation in Scala, which is the only widely available statically typed OOP language with a sufficiently powerful type system needed to support FOP.
This new work also describes some composition mechanisms for object algebras in the context of more expressive languages.
The ECOOP 2012 best paper award this year was given to Bruno Oliveira and William Cook for the paper "Extensibility for the Masses: Practical Extensibility with Object Algebras".
This paper is (yet another) solution to the expression problem. The basic idea is that you create a family of objects via an Abstract Factory. You can add new objects to the family by extending the factory as per usual, but the twist is you can also add new operations by overriding the factory methods to do other things, like evaluation or pretty printing.
Bruno has also been collecting sample implementations using Object Algebras solving a simple expression problem example.
And let me also repeat CBPV's slogan, which is one of the finest in PL advocacy: Once the fine structure has been exposed, why ignore it?
Ongoing discussion that you can follow on William Cook's blog.
I am not going to take sides (or keep points). I know everyone here has an opinion on the issue, and many of the arguments were discussed here over the years. I still think LtU-ers will want to follow this.
Given the nature of the topic, I remind everyone to review our policies before posting here on the issue.
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter, Speciﬁcation and Veriﬁcation: The Spec# Experience" Preprint of an article appearing in the June 2011 CACM.
CACM tagline: Can a programming language really help programmers write better programs?
Spec# is, in some ways, quite similar to JML+ESC/Java2. But Spec# is a language rather than a set of annotations, which allows it to incorporate features such as a non-null type system and a very tight integration with the IDE.
Spec# was previously mentioned on LtU back in 2005.
Parametric Prediction of Heap Memory Requirements, by Victor Braberman, Federico Fernandez, Diego Garbervetsky, Sergio Yovine:
We've briefly discussed analyses to predict heap usage here on LtU, but I can't seem to find them. Anyone with a reference handy, please post in the comments!
Oleg just posted a new page, First-class modules: hidden power and tantalizing promises, related to new features in OCaml 3.12 (on LtU).
It includes a nice intro to first-class modules by Frisch and Garrigue: First-class modules and composable signatures in Objective Caml 3.12.
OCaml definitely just got even more interesting.
Objects to Unify Type Classes and GADTs, by Bruno C. d. S. Oliveira and Martin Sulzmann:
A very interesting paper on generalizing and unifying type classes and GADTs. Classes are now first-class values, resulting in a language that resembles a traditional, albeit more elegant, object-oriented language, and which supports a form of first-class "lightweight modules".
The language supports the traditional use of implicit type class dispatch, but also supports explicit dispatch, unlike Haskell. The authors suggest this could eliminate much of the duplication in the Haskell standard library of functions that take a type class or an explicit function, eg. insert/insertBy and sort/sortBy, although some syntactic sugar is needed to make this more concise.
Classes are open to extension by default, although a class can also be explicitly specified as "sealed", in which case extension is forbidden and you can pattern match on the cases. Furthermore, GADTs can now also carry methods, thus introducing dispatch to algebraic types. This fusion does not itself solve the expression problem, though it does ease the burden through the first-class support of both types of extension. You can see the Scala influences here.
I found this paper via the Haskell sub-reddit, which also links to a set of slides. The authors acknowledge Scala as an influence, and as future work, suggest extensions like type families and to support more module-like features, such as nesting and opaque types.
Joe-E: A Security-Oriented Subset of Java. Adrian Mettler, David Wagner, and Tyler Close. To appear at ISOC NDSS 2010.
We present Joe-E, a language designed to support the development of secure software systems. Joe-E is a subset of Java that makes it easier to architect and implement programs with strong security properties that can be checked during a security review. It enables programmers to apply the principle of least privilege to their programs; implement application-specific reference monitors that cannot be bypassed; introduce and use domain-specific security abstractions; safely execute and interact with untrusted code; and build secure, extensible systems. Joe-E demonstrates how it is possible to achieve the strong security properties of an object-capability language while retaining the features and feel of a mainstream object-oriented language...
Section 5.2 discuss how Joe-E leverages Java static typing. Joe-E is implemented as a source-code verifier not a bytecode verifier. Section 6 of the paper explains this design choice.
Active forum topics
New forum topics