Graded Inference Resource Aware Logical Framework

A Modern Implementation of Automatic Amortized Resource Analysis

Collaborators

Languages Involved

  • Implementation: OCaml, Agda
  • Source: Giralf (Custom)

Overview

  • Designed a Call-by-Push-Value (CBPV) based language (Giralf) with the cost effect and accompanying substructural type system
  • Collaborated with authors of DeCalf to develop a categorical semantics encoding the soundness of AARA on Giralf into DeCalf
  • Implemented in Agda a verified compiler from Giralf into a DeCalf proof of a resource bound on the original Giralf program
  • Added an interface with RaML2, thus supporting a complete pipeline that infers then verifies resource bounds on SML programs
  • Currently supports linear resource bounds, working toward polynomial resource bound