Rippling: a heuristic for guiding inductive proofs

It assumes that, which is actually true in most induction, the conclusion and hypothesis have almost the same structure(also called skeleton).
So rippling just convert each inferring rules of this reasoning system into a new rewriting rule, which transforms formulas with the same skeleton.
Such transformation is very similar to the rippling wave on the water surface, which is the source of the name rippling.

SOSP11: PTask: Operating System Abstractions To Manage GPUs as Compute Devices

This paper provide a dataflow programming model by designing a Ptask API, which describe the dataflow between varias cmputing tasks.

These tasks can be schedule on to GPU as well as CPUs. In this way, non-neccesarry copy between devices, drivers and user codes are avoid, and the user does not need to care about the data movement explictly.

SOSP11:Scalable Consistency in Scatter

There are so many papers that discuss the key-value storage, their consistency and scalability .

But I can't go into this topic because I dont have access to such environment.