Resource Aware ML

I am actively developing Resource Aware ML (RAML), an ML-like functional programming language that implements an automatic static analysis of the quantitative resource requirements of a program.

For instance, RAML automatically derives symbolic worst-case bounds on memory and time usage of programs such as quick sort for lists of lists, in-place quick sort for arrays, Dijkstra's shortest-path algorithm, matrix operations, and longest common subsequence of two lists. The analysis is highly efficient and takes only a few seconds for the aforementioned programs.

We are constantly improving the range and the precision of the analysis. In the development of RAML we apply techniques from many interesting areas such as type systems, static analysis, constraint solving, analysis of algorithms, and design and implementation of programming languages.

Collaborators: See

Analyzing Probabilistic Programs

Resource Aware Session Types

Collaborators: Ankush Das and Frank Pfenning.

High-Assurance Smart Contracts

Collaborators: Andrew Miller and Bryan Parno.

Resource-Guided Program Synthesis

Collaborators: Nadia Polikarpova and Benjamin Lichtman.