This is the submission to the PLDI 2014 Artifact Evaluation Committee for the paper:

We submit three artifacts:

  1. A machine-checked formalizations of our theoretical results, in the dependently-typed programming language Agda.

  2. A prototype implementation of our ideas in Scala.

  3. The raw data and detailed graphs of our benchmark.

Quick Start

The virtual machine contains everything you need to interact with our artifacts:

More information about the virtual machine image is available below.

Other Download Options

The Virtual Machine image (see below) is probably the easiest way to interact with our artifacts, but we also provide the following alternatives:

Virtual Machine Image

The following virtual machine image contains all artifacts as well as the software we used to create and use the artifacts. Except maybe for Agda or Scala power users, this is probably the easiest way to interact with the artifacts.

This virtual machine contains a Ubuntu system. Inside the virtual machine, you will also find on the desktop:

How to interact with the Agda codebase

On the left-hand side you will also find links for Emacs and a terminal; Emacs is already set up for working with Agda, and the Agda README contains basic instructions for working with Emacs and for finding more information.

On the desktop, there’s a link to the Agda README which will open in Emacs.

How to interact with the Scala codebase

For compiling the Scala codebase and running tests, we preinstalled SBT and configured it to have enough memory (1G) and stack (8M) to compile and run our code with the big datasets we use. We reduced the maximum benchmark size to fit the virtual machine memory - we originally ran them with 4G of RAM on a 64bit virtual machine, but we preferred creating a 32bit VM with less RAM. Details on how to change the configuration are in the README for the Scala codebase.

We also preloaded Eclipse with the correct version of the Scala plugin (Scala IDE 3.0.2) on the virtual machine, and preloaded our project for it. However, Eclipse cannot compile the project from scratch unless SBT has already compiled the source code before. So for example, you have to compile with SBT once after each “clean” in Eclipse.

Virtual machine survival guide

The VM is a mostly standard Ubuntu Linux 12.04 LTS system. Should you be unfamiliar with Ubuntu, or should you need info on the configuration, here is some survival information which might get you started.

Why VirtualBox 4.3.6?

We package the virtual machine in the standardized OVF format. Therefore, at least in theory the virtual machine should work with other versions of VirtualBox. It should even work with VMWare, though the guest contains optimized drivers for VirtualBox (VirtualBox Guest Additions 4.3.6) but not for VMWare (so it will at least be less performant on VMWare).

However, we have only tested running the VM on OS X, Windows and Linux systems with VirtualBox 4.3.6, and workarounded the VirtualBox bugs we did find (we had to disable 3D acceleration to ensure scrolling would work in Emacs). Whether other VirtualBox versions will work depends entirely on VirtualBox and is outside of our control — even though usually VirtualBox does work.