Verifiable Functional Purity in Java. Matthew Finifter, Adrian Mettler, Naveen Sastry, and David Wagner. To appear at 15th ACM Conference on Computer and Communication Security (CCS 2008).
Proving that particular methods within a code base are functionally pure - deterministic and side-effect free - would aid verification of security properties including function invertibility, reproducibility of computation, and safety of untrusted code execution. Until now it has not been possible to automatically prove a method is functionally pure within a high-level imperative language in wide use such as Java. We discuss a technique to prove that methods are functionally pure by writing programs in a subset of Java called Joe-E; a static verifier ensures that programs fall within the subset. In Joe-E, pure methods can be trivially recognized from their method signature.
The paper includes a nice discussion of security benefits that can stem from being able to identify pure functions (of course, it is not obvious that guarantees at the programming language level are maintained at the run time level). I am sure many here have opinions about whether it makes more sense to try to graft purity on an imperative language, exposing it as an added feature, or to move programmers to functional languages..
UpgradeJ: Incremental Typechecking for Class Upgrades, Gavin Bierman, Matthew Parkinson and James Noble.
There has been an energetic discussion of API evolution in the forum, so when I saw this paper I thought it might be of interest to LtU readers.
I just noticed Stroustrup is about to publish this introductory book.
I am stunned on many levels, so I will keep my comments short.
In general, this seems like HTDP for C++, that is it is not a comprehensive text about C++ or about CS in general, but rather one aimed at teaching the basics of software construction. This is a good idea, and many have written books with similar goals in the past, of course.
I wonder what are the chances that any university not employing Stroustrup will switch to C++ for their introductory course (if they are not using it already). It seems to me everyone is teaching Java...
My second observation is that a large fraction of the book is devoted to STL. Which a good thing on many levels. Some of the topics may even be explained functionally.
My third observation is that even given the intended audience and goals the ToC seems really sparse. I wonder if that's all the book is going to contain.
Eriskay: a Programming Language Based on Game Semantics. John Longley and Nicholas Wolverson. GaLoP 2008.
It's always interesting to see a new programming language strongly based on some mathematical formalism, because a language gives you a concrete example to match the abstract semantic definitions to, and game semantics is something that I've been curious about for a while.
One particularly interesting feature is that the core language has a restricted model of the heap, which controls the use of higher-order store in such a way that cycles are prohibited. This is enforced with a notion called "argument safety", which essentially prohibits storing values of higher type into fields which come from "outside" the object. This is somewhat reminiscent of the ownership disciplines found in OO verification systems like Boogie, which enforce a tree structure on the ownership hierarchy. It would be very interesting to find out whether this resemblance is a coincidence or not.
(Samson Abramsky has some lecture notes on game semantics for the very curious.)
Jumbala : An Action Language for UML State Machines, Juro Dubrovin, Master's Thesis.
This is interesting because it is another example of efforts from the modeling community towards combining models and programming languages to provide a single compilable specification of software. Some of these efforts are being coordinated using the term model-driven architecture (MDA).
[edit: fixed formatting issues]
In my recent adventures researching modeling languages I came across a language not previously mentioned on Lambda-the-Ultimate.org called Kermeta. From the reference manual:
There is a list of published papers related to Kermeta here.
Peter Pirkelbauer, Yuriy Solodkyy, and Bjarne Stroustrup. Open Multi-Methods for C++. Proc. ACM 6th International Conference on Generative Programming and Component Engineering (GPCE). October 2007.
Multiple dispatch â€“ the selection of a function to be invoked based on the dynamic type of two or more arguments â€“ is a solution to several classical problems in object-oriented programming. Open multi-methods generalize multiple dispatch towards open-class extensions, which improve separation of concerns and provisions for retroactive design. We present the rationale, design, implementation, and performance of a language feature, called open multi-methods, for C++ . Our open multi-methods support both repeated and virtual inheritance... ...our approach is simpler to use, catches more user mistakes, and resolves more ambiguities through link-time analysis, runs significantly faster, and requires less memory. In particular, the runtime cost of calling an open multimethod is constant and less than the cost of a double dispatch (two virtual function calls). Finally, we provide a sketch of a design for open multi-methods in the presence of dynamic loading and linking of libraries.
Who said C++ isn't evolving?
The discussion in section 4 of the actual implementation (using EDG) is particularly detailed, which is a bonus.
A short audio presentation (Avi speaks for less than ten minutes, I guess), about the lessons the Ruby community should learn from Smalltalk. It's mainly about turtles-all-the-way-down, but Self (fast VMs), GemStone (transactional distributed persistence), Seaside (web frameworks) are also mentioned briefly.
Vaidas Gasiunas, Mira Mezini, Klaus Ostermann. Dependent Classes. OOPSLA'07.
Virtual classes allow nested classes to be refined in subclasses. In this way nested classes can be seen as dependent abstractions of the objects of the enclosing classes. Expressing dependency via nesting, however, has two limitations: Abstractions that depend on more than one object cannot be modeled and a class must know all classes that depend on its objects. This paper presents dependent classes, a generalization of virtual classes that expresses similar semantics by parameterization rather than by nesting. This increases expressivity of class variations as well as the flexibility of their modularization. Besides, dependent classes complement multimethods in scenarios where multi-dispatched abstractions rather than multi-dispatched methods are needed. They can also be used to express more precise signatures of multimethods and even extend their dispatch semantics. We present a formal semantics of dependent classes and a machine-checked type soundness proof in Isabelle/HOL, the first of this kind for a language with virtual classes and path-dependent types.I enjoyed this talk at OOPSLA, although I was not able to see the end, and I enjoyed the paper even more. There's been so much work on virtual classes in recent years, and while I very clearly see a strong practical motivation for this work, I admit that I find it difficult to keep track of the technical trade-offs between different approaches. This, plus the persistent limitations mentioned in the abstract, lends some of the papers an unfortunately tedious feel (to me). I find this work refreshing, since it introduces a substantial new idea in this area. (And of course, one of the authors posts here regularly...)
You can browse the LaTex files in the svn repository.
Active forum topics
New forum topics