Resource Aware ML (RAML) is a (first-order) functional programming language that fully automatically computes polynomial resource bounds at compile time.

It is based on an automatic type-based amortized analysis that is generic in the resource of interest.

In this prototype implementation we use two machine independent resource metrics: heap-space consumption and evaluation steps in the big-step semantics. 

News

• 31/03/2012: New RAML Release

  We are happy to announce the release of version 0.7 of Resource Aware ML. The new version runs about 4 times faster than version 0.6x. The speed improvement is due to a reduction of the number of generated constraints and to changes in the Haskell implementation.

  The new version also implements an often requested feature: the output of the resource types that are used for function applications. Details can be found in the documentation section.

• 24/03/2012: Tool Demo at CAV'12

  Our (Jan, Klaus and Martin) tool paper on Resource Aware ML has been accepted for publication at the International Conference on Computer Aided Verification (CAV'12). We hope to see you at our tool demo in Berkeley in July.

• 24/02/2012: RAML and Cabal

  Johannes Waldmann created a a RAML Cabal package. This makes the installation of RAML very easy. Just run the following commands.

  git clone git://dfa.imn.htwk-leipzig.de/srv/git/raml
  cabal configure && cabal build

  To test the installation run the following.

  ./dist/build/raml/raml analyse eval-steps 4 examples/matrix.raml

• 23/11/2011: New Examples

  We implemented all examples form the paper The Size-Change Principle for Program Termination that have a polynomial running time (5 of 6). All examples are tricky to prove terminating but you can prove termination by using the size-change principle.

  These 5 examples can be automatically analyzed in RAML and the computed bounds are all asymptotically tight. Select the example file sizechange.raml from the drop-down menu on the prototype page for details.

• 21/11/2011: Dissertation Online

  On October 14, Jan successfully defended his doctoral thesis. His dissertation with the title Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis is now available online. It contains a thorough informal introduction to our research.