Lambda the Ultimate

Celebrating Niklaus Wirth's 80th Birthday, 20th Feb 2014.

Niklaus Wirth was a Professor of Computer Science at ETH Zürich, Switzerland, from 1968 to 1999. His principal areas of contribution were programming languages and methodology, software engineering, and design of personal workstations. He designed the programming languages Algol W, Pascal, Modula-2, and Oberon, was involved in the methodologies of structured programming and stepwise refinement, and designed and built the workstations Lilith and Ceres. He published several text books for courses on programming, algorithms and data structures, and logical design of digital circuits. He has received various prizes and honorary doctorates, including the Turing Award, the IEEE Computer Pioneer, and the Award for outstanding contributions to Computer Science Education.

We celebrated Niklaus Wirth's 80th birthday at ETH Zürich with talks by Vint Cerf, Hans Eberlé, Michael Franz, Bertrand Meyer, Carroll Morgan, Martin Odersky, Clemens Szyperski, and Kathleen Jensen. Wirth himself gave a talk about his recent port of Oberon onto a low-cost Xilinx FPGA with a CPU of his own design.

The webpage includes videos of the presentations.

Junfeng Yang, Heming Cui, Jingyue Wu, Yang Tang, and Gang Hu, "Determinism Is Not Enough: Making Parallel Programs Reliable with Stable Multithreading", Communications of the ACM, Vol. 57 No. 3, Pages 58-69.

We believe what makes multithreading hard is rather quantitative: multithreaded programs have too many schedules. The number of schedules for each input is already enormous because the parallel threads may interleave in many ways, depending on such factors as hardware timing and operating system scheduling. Aggregated over all inputs, the number is even greater. Finding a few schedules that trigger concurrency errors out of all enormously many schedules (so developers can prevent them) is like finding needles in a haystack. Although Deterministic Multi-Threading reduces schedules for each input, it may map each input to a different schedule, so the total set of schedules for all inputs remains enormous.

We attacked this root cause by asking: are all the enormously many schedules necessary? Our study reveals that many real-world programs can use a small set of schedules to efficiently process a wide range of inputs. Leveraging this insight, we envision a new approach we call stable multithreading (StableMT) that reuses each schedule on a wide range of inputs, mapping all inputs to a dramatically reduced set of schedules. By vastly shrinking the haystack, it makes the needles much easier to find. By mapping many inputs to the same schedule, it stabilizes program behaviors against small input perturbations.

The link above is to a publicly available pre-print of the article that appeared in the most recent CACM. The CACM article is a summary of work by Junfeng Yang's research group. Additional papers related to this research can be found at http://www.cs.columbia.edu/~junfeng/

It is increasingly important for applications to protect user privacy. Unfortunately, it is often non-trivial for programmers to enforce privacy policies. We have developed Jeeves to make it easier for programmers to enforce information flow policies: policies that describe who can see what information flows through a program. Jeeves allows the programmer to write policy-agnostic programs, separately implementing policies on sensitive values from other functionality. Just like Wooster's clever valet Jeeves in Wodehouse's stories, the Jeeves runtime does the hard work, automatically enforcing the policies to show the appropriate output to each viewer.

From what I gather, Jeeves takes Aspect Oriented approach to privacy. This is of course not a new idea. I presume that many of the classic problems with AOP would apply to Jeeves. Likewise, using information flow analysis for handling privacy policies is not an new idea. Combining the two, however, seems like a smart move. Putting the enforcement at the run-time level makes this sound more practical than other ideas I have heard before. Still, I personally think that specifying privacy policies at the end-user level and clarifying the concept of privacy at the normative, legal and conceptual levels are more pressing concerns. Indeed, come to think of it: I don't really recall a privacy breach that was caused by a simple information flow bug. Privacy expectations are broken on purpose by many companies and major data breaches occur when big databases are shared (recall the Netflix Prize thing). Given this, I assume the major use-case is for Apps, maybe even as a technology that someone like Apple could use to enforce the compliance of third-party Apps to their privacy policies.

I haven't looked too closely, so comments from more informed people are welcome.

Jeeves is implemented as an embedded DSL in Scala and Python.

CK Hur, D Dreyer, G Neis, V Vafeiadis (POPL 2012). The marriage of bisimulations and Kripke logical relations.

There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are bisimulations and Kripke logical relations (KLRs). While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to inter-language reasoning.

In this paper, we propose relation transition systems (RTSs), which marry together some of the most appealing aspects of KLRs and bisimulations. In particular, RTSs show how bisimulations' support for reasoning about recursive features via coinduction can be synthesized with KLRs' support for reasoning about local state via state transition systems. Moreover, we have designed RTSs to avoid the limitations of KLRs and bisimulations that preclude their generalization to inter-language reasoning. Notably, unlike KLRs, RTSs are transitively composable.

I understand the paper as offering an extension to bisimulation that handles the notion of hidden transitions properly and so allows a generalisation of KLRs to any systems that can be treated using bisimulations. Applications to verified compilation are mentioned, and everything has been validated in Coq.

Matt Pharr, Greg Humphreys, and Pat Hanrahan have recently been given an Academy Award for Technical Achievement, for the book Physically Based Rendering. This is the first time the award has been given to a book and (more relevant to LtU) the first time a literate program has won an Academy Award.

The proceedings can be downloaded from the POPL webpage.

I find this extremely exciting (not only because I didn't get funds to attend POPL this year). To my knowledge, this is the first time that this is done in POPL/ICFP/PLDI; electronic proceedings were previously only delivered to attendees, with an explicit request not to share them.

I am not sure what is the reasoning that make which people decide to do it this year, or not to do it before. I hope that the proceedings will remain available after the conference (next week), and that this idea will be adopted for the years to come.

Multiple Dispatch as Dispatch on Tuples, by Gary T. Leavens and Todd D. Millstein:

Many popular object-oriented programming languages, such as C++, Smalltalk-80, Java, and Eiffel, do not support multiple dispatch. Yet without multiple dispatch, programmers find it difficult to express binary methods and design patterns such as the "visitor" pattern. We describe a new, simple, and orthogonal way to add multimethods to single-dispatch object-oriented languages, without affecting existing code. The new mechanism also clarifies many differences between single and multiple dispatch.

Multimethods and multiple dispatch has been discussed numerous times here on LtU. While the theory has been fully fleshed out to the point of supporting full-fledged type systems for multiple dispatch, there has always remained a conceptual disconnect between multimethods and the OO model, namely that methods are supposed to be messages sends to objects with privileged access to that object's internal state. Multimethods would seem to violate encapsulation inherent to objects, and don't fit with the conceptual messaging model.

This paper goes some way to solving that disconnect, as multiple dispatch is simply single dispatch on a distinct, primitive class type which is predicated on N other class types and thus supporting N-ary dispatch. This multiple dispatch support can also be retrofitted to an existing single-dispatch languages without violating its existing dispatch model.

Interesting and wide-ranging interview with Adele Goldberg from Computer History
Transcript and Video at Computer History Also on YouTube

Adele Goldberg reflects on her life and career from her early days at the University of Chicago and Stanford University through her career at Xerox Palo Alto Research Center (PARC) and ParcPlace Systems.

Another Oral History interview with her by IEEE Global History Network

Goldberg discusses her educational and work history. She recalls her experiences as a student at the University of Michigan and at the University of Chicago. Next, she covers her stretch at Xeorx PARC, sharing her views on the work environment. Here she speaks at length about her work on Smalltalk, including her leading role in its commercialization. Goldberg is candid about the challenges she faced in forming and running spin-out company ParcPlace Systems. In addition, she discusses her two-year tenure as President of ACM. Finally, Goldberg offers advice for young women who are considering a career in computing.

I haven't seen this discussed here yet: http://www.puzzlescript.net/

It is an HTML5-based puzzle game engine that uses a simple language for patterns and substitutions to describe game rules. For example (taken from their introduction), the basic block-pushing logic of a Sokoban game can be given as:

[ > Player | Crate ] -> [ > Player | > Crate ]

This line says that when the engine sees the pattern to the left of ->, it should replace it with the pattern on the right. In this case, the rule can be read as something like: when there is a row or column ([]) that contains a player object (Player) next to (|) a crate object (Crate), and the player is trying to move toward the crate (>), then (->) make the crate move in the same direction.

Rules are matched and applied iteratively at each step (i.e., when the player acts), until there are no more matches, and then movement takes place. There are mechanisms for influencing the order in which rules are run, and for forcing subsets of the rules to be iterated. By default, rules apply to both rows and columns, but horizontal- or vertical-only rules can be created.

It is an interesting example of a very narrowly-focused DSL, based on a (relatively) uncommon model of computation. It's also very fun to play with!

Backpack: Retrofitting Haskell with Interfaces
Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones, Simon Marlow
2014

Module systems like that of Haskell permit only a weak form of modularity in which module implementations directly depend on other implementations and must be processed in dependency order. Module systems like that of ML, on the other hand, permit a stronger form of modularity in which explicit interfaces express assumptions about dependencies, and each module can be typechecked and reasoned about independently.

In this paper, we present Backpack, a new language for building separately-typecheckable packages on top of a weak module system like Haskell's. The design of Backpack is inspired by the MixML module calculus of Rossberg and Dreyer, but differs significantly in detail. Like MixML, Backpack supports explicit interfaces and recursive linking. Unlike MixML, Backpack supports a more flexible applicative semantics of instantiation. Moreover, its design is motivated less by foundational concerns and more by the practical concern of integration into Haskell, which has led us to advocate simplicity—in both the syntax and semantics of Backpack—over raw expressive power. The semantics of Backpack packages is defined by elaboration to sets of Haskell modules and binary interface files, thus showing how Backpack maintains interoperability with Haskell while extending it with separate typechecking. Lastly, although Backpack is geared toward integration into Haskell, its design and semantics are largely agnostic with respect to the details of the underlying core language.