I already reviewed the other Thorn paper, Thorn—Robust, Concurrent, Extensible Scripting on the JVM. This one just goes into more detail on the type system, and how like-types interact with dynamic and static types. I like the idea of minimizing the impact of converting part of your code to being type checked, as a step toward making your whole program statically typed.

Source: PDF ACM

Another crazy use of type systems. Here the idea is to completely ignore the declared types of variables and instead just run a type inference algorithm (Milner’s Algorithm W) on the program and see what types you get. Instead of using primitive operations (like addition) to constrain variables to representation types (like int), you just constrain variables to the same type. Naturally, assignment and function calls cause type unification as well. You end up with a bunch of abstract types assigned to variables that reflect whether they are “related”. The idea is that this helps you to understand where values flow through your program and what might be impacted when making changes. It sounds like an interesting idea; I have no idea if it would be useful in practice.

Source: PDF ACM

This is a follow-up to Milner’s introduction of the type inference algorithm known as Hindley-Milner or Algorithm W. Here they provide a sketch of a proof that it infers “principal” types which are the most general possible types. (This proof was given by Hindley over a decade earlier, but apparently Milner nor the any of the reviewers knew about it.) It’s the sort of paper that wastes no ink on pesky prose explanations of the nice compact formulas, which is great for the trees, but really annoying when any of those formulas contain typos. If you’re not already familiar with the subject matter, you might spend an awful lot of time trying to figure out whether they really meant theta-sub-one when they wrote theta-sub-two.

Source: PDF ACM

More fun with type systems! Here they use type annotations to distinguish between pointers under user control and pointers under kernel control, and type inference to allow them to only add annotations on system calls and on functions where passing a user pointer is safe and where it’s not. The type inference fills in everything in between, or rather specifically identifies places where user pointers are used unsafely. They then run this on all 1.4 million lines of the Linux kernel. That’s a pretty impressive case study.

One of the cool things about this paper is that they mostly focus on how they improved an existing analysis tool to eliminate false positives (as well as characterizing the false positives they were unable to avoid), which provides object lessons in why you care about things like context sensitivity, flow sensitivity, field sensitivity, and so forth.

Source: PS ACM

Describes a library for .NET that introduces constructs for lightweight parallel programming, mainly Parallel.For and Parallel.Aggregate. These are parallel for-loops and fork/join (also popularly known as map/reduce). Unlike DPJ, these guys don’t provide a type system or any guarantees that you’re not shooting yourself in the foot. They claim those are “orthogonal concerns” which is a bit of a cop-out, but not totally. For parallel for-loop kind of stuff, you probably are doing something mostly safe. For fork/join and their more flexible basic futures, you’re free to use those in all sorts of naive ways and not realize that you have race conditions coming out of your proverbial orifices. In any case, they describe their implementation, which is cool.

Source: PDF ACM

Describes a points-to analysis expressed entirely as a Datalog program. (Datalog is awesome!) They focus on the optimizations done to the Datalog program to allow the analysis to be faster and more scalable than the state-of-the-art (the paper being from OOPSLA 2009). The existing techniques have moved toward using BDDs to improve scalability and these guys are keen to prove that to be a bad idea.

Source: PDF ACM

Extends the work described in Points-to Analysis in Almost Linear Time, which didn’t handle structs or unions (all this is for C). Unfortunately, C’s “type system” makes this work very messy because they need to account for all the nasty things you can do with structs (like overwrite two adjacent int fields by assigning through a long pointer). Sausage making indeed.

Source: PDF ACM

Describes a cool technique for turning a points-to analysis into a type inference problem—one that can be done in almost linear time, hence the title. As type checking is flow-insensitive, so is the analysis, and since it infers monomorphic types, the analysis is also context-sensitive, but there’s nothing stopping you from doing a polymorphic inference and getting a context sensitive analysis (which I think Steensgaard later did).

Source: PDF ACM