Bernie Pope

Programming Languages Workshop 2011


Tuesday 29 November 2011, 1.00-6.30pm.


The University of Melbourne
Theatre 3 (Second Floor, Room 205) ICT Building
111 Barry Street, Carlton



The Properties of Riak

John Hughes

Riak is one of the new breed of no-SQL database management systems, which has begun to replace relational databases for some applications. Riak is a distributed key-value store, inspired by Amazon’s Dynamo, designed for applications where scalability, low latency and high availability are critical. Riak uses replication to provide fast access to data, even when multiple nodes or parts of the network fail. It supports concurrent access to the same data by multiple clients, even when the network is partitioned. All of this makes it very hard to test.

I will show how QuickCheck helped us to model Riak’s behavior, improving understanding and revealing the occasional bug.

Giving Haskell a Promotion

Simon Peyton Jones

Static type systems strive to be richly expressive while still being simple enough for programmers to use. We describe an experiment that enriches Haskell’s kind system with two features promoted from its type system: data types and polymorphism. The new system has a very good power-to-weight ratio: it offers a significant improvement in expressiveness, but, by re-using concepts that programmers are already familiar with, the system is easy to understand and implement.

Constraint Logic Programming with Learning

Peter Stuckey

Constraint logic programming (CLP) is the archetypal constraint programming language (scheme). It allows the specification of constraint problems as well as search strategies in a clear and simple manner. But most modern constraint programming systems are not CLP systems, instead they allow a fixed set of constraints to be specified, and search to be controlled using a different language. Recently CP systems have been substantially improved by the addition of learning techniques. Learning records sets of decisions that do not lead to a solution and avoid repeating the same set of decisions. In this talk we extend learning techniques to CLP systems, which allows the same search benefits to be derived for more complex kinds of hierarchical search.

Succinct Data Structures in Haskell

Andrew Bromage

Data structure compression differs from traditional data compression in that the compressed data does not need to be decompressed to do useful work with it. Moreover, many common data structures can be implemented in space which is very close to optimal. This talk is a brief introduction to the field, with example code in Haskell.

Undefinedness and Underspecification

Lee Naish

At the core of programming is the relationship between what is computed and what we intend to compute. To describe precisely what is computed by any reasonably expressive system, some notion of undefinedness is essential. We have known there are limits to what can be formally defined and computed since the work of Gödel and Turing. To describe precisely what we intend to compute, some notion of underspecification is essential to express concepts such as “garbage in” and “pre-conditions”. This has been known since the time of Babbage. Drawing on recent work in logic programming, we argue that undefinedness is the dual of underspecification and having a framework which incorporates both concepts is desirable.

Meaningful Programming

Bill Birch

Evolving programming languages to integrate with the Semantic Web and its underlying concepts. We will start with Lisp 1 and describe what happens when SemWeb ideas are merged with it. What could be the benefits? What’s the implication of a type system based on Description Logics?

Mars: An Imperative/Declarative Programming Language Prototype

Matt Giuca

For years, we have enjoyed the robustness of programming without side-effects in languages such as Haskell and Mercury. Yet in order to use languages with true referential transparency, we seem to have to give up basic imperative constructs that we have become accustomed to: looping constructs, variable update, destructive update of arrays, and so on. In my programming language, Mars, the programmer is allowed to write imperative-style code using Python syntax, yet has the benefits of a language with referential transparency. An unreleased version of Mars performs analysis to automatically perform destructive update of arrays wherever possible.

I will give a demo of this prototype language, and show some of the new features since my previous talk, including the automatic destructive update. I also discuss the design philosophy behind the language, and its future directions.

Controlling Loops in Parallel Mercury Code

Paul Bone

Recently we built a system that uses profiling data to automatically parallelize Mercury programs by finding conjunctions with expensive conjuncts that can run in parallel with minimal synchronization delays. This worked very well in many cases, but in cases of tail recursion, we got substantially lower speedups than we expected, due to excessive memory usage. In this paper, we present a novel program transformation that eliminates this problem, and for the first time allows recursive calls inside parallel conjunctions to take advantage of tail recursion optimization. Our benchmark results show that our new transformation greatly increases the speedups we can get from parallel Mercury programs. In some cases, it doubles the speedup, and in one case, it increases it by almost a factor of four, from no speedup to almost perfect speedup on four cores.

Congruence Analysis with Bit-Precise Transfer Functions

Harald Søndergaard

The talk is about analysis and verification of programs that use bit-twiddling for numerical computation over fixed-width integers. Using a technique first proposed by Reps, Sagiv and Yorsh, we show how local, bit-precise analysis can be used to enhance congruence analysis. Escaping the usual restriction to linear assignments, such analysis enables automated verification of bit-manipulating programs, without necessarily incurring excessive cost. The work presented has been done jointly with Andy King.