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.
Establishing Object Invariants with Delayed Types. Manuel Fähndrich, Songtao Xia.
It's interesting to note that in Ada type definitions can contain initializers (i.e., initialization expressions), partly because constructors were introduced into the language only in the second revision of the language (Ada95).
Validity Invariants and Effects, Yi Lu, John Potter and Jingling Xue. ECOOP 2007.
I really liked this paper, but I think it might need a few preliminary explanations. There's a style of verification of OO programs based on "object invariants", which is the idea that you ensure that each object has an invariant, which every method maintains. Then verification is local, in the sense that you can verify each class's invariants independently. (This is used in the Boogie methodology used by Spec#, for instance.)
However, there are a couple of wrinkles. First, aliasing: every object's invariant depends on some of the objects in its fields, and you don't want random aliases letting strangers modify your representation objects underneath your feet. So you introduce a notion of ownership to help track who has permission to mess with each object. Second, reentrancy: suppose the middle of a method body has temporarily broken the object's invariant, and you call another method on the object? You don't a priori know the call is safe.
The type system the authors have introduced here tracks ownership and possibly-dangerous reentrant calls. The really clever part is that instead of just rejecting programs that fail these checks, they log all of the places where things break. So instead of saying "yes" or "no", the type system says "yes" or "manually verify the following things". So it's a labor-saving device for a verification methodology.
Morphing: Safely Shaping a Class in the Image of Others, Shan Shan Huang, David Zook, and Yannis Smaragdakis. ECOOP 2007.
This is related to the paper by Turon and Reppy I linked to yesterday; it's another take on compile-time metaprogramming. This time they have a static iteration over the structure of a class, which makes their safety result rather impressive. I talked Huang, and she told me that their big-picture goal is to eventually build a full language for manipulating programs at compile time, while still preserving all the safety guarantees we expect.
Active forum topics
New forum topics