Auction Theory Toolbox – Isabelle (generated Scala code)

Verified code generated from the Isabelle formalisation

How to run

  1. For just executing the generated code, obtain Scala (see below), or use Java with a recent version of scala-library.jar, e.g. scala-library-2.10.2. Then follow the instructions in README.
  2. For building the code, obtain Isabelle and Scala. Our formalisation is known to work with Isabelle2013-1-RC1; the generated code is known to work with Scala 2.10.
  3. You currently need to manually load and run any of the Isabelle theories that generate code (check the overview for “code”), e.g. in jEdit.
  4. The Makefile has several relevant targets; e.g., you can build and run the CAB example as follows:
    1. make CombinatorialVickreyAuctionCAB.class
    2. scala CombinatorialVickreyAuctionCAB < example.cab
  5. For executing split-scala-modules.pl (required by the Makefile), you need Perl ≥5.10 with the File::Spec module.

This page was last modified on 04 October 2013.