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

• 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.

• 08/10/2011: New RAML Release

  We are happy to release version 0.6 of the prototype. It contains small fixes and some new features that make the prototype more usable.

  The most visible novelty is the introduction of a new ticks metric which allows users to define the resource consumption of programs. You can now use expressions such as let _ = tick(2.34) in e if you want to define that the expression e consumes 2.34 resources.

• 13/09/2011: Talk

  Jan talks about Polynomial Amortized Resource Analysis at the Laboratoire PPS at the Université Paris 7 - Denis Diderot.

• 01/08/2011: New Paper

  We submitted a draft of the full version of our POPL'11 paper on Multivariate Amortized Resource Analysis.