Hector Suzanne

An automated resource analysis technique is introduced, targeting a Call-By-Push-Value abstract machine, with memory prediction as a practical goal. The machine has a polymorphic and linear type system enhanced with a first-order logical fragment, which encodes both low-level operational semantics of resource manipulations and high-level synthesis of algorithmic complexity. Resource analysis must involve a diversity of static analysis, for escape, aliasing, algorithmic invariants, and more. Knowing this, we implement the Automated Amortized Resource Analysis framework (AARA) from scratch in our generic system. In this setting, access to resources is a state-passing effect which produces a compile-time approximation of runtime resource usage. We implemented type inference constraint generation for our calculus, accompanied with an elaboration of bounds for iterators on algebraic datatypes, for minimal ML-style programming languages with Call-by-Value and Call-By-Push-Value semantics. The closed-formed bounds are derived as multivariate polynomials over the integers. This now serves as a base for the development of an experimental toolkit for automated memory analysis of functional languages.

My PhD research focuses on compile-time prediction of memory usage for programs written in functional-imperative style, following the technique of Automated Amortized Resource Analysis.

The approach is based on an intermediate representation for a virtual machine, with the following features:

• Call-By-Push-Value: it allows both javascript- and Haskell-style functional programming, where evaluating data is done eagerly, and composing computations is done lazily. Those two polarities can be judiciously combined to encode efficient iterations and data processing workflows in an imperative style, which are compiled as purely functionnal programs for the VM.
• Linear type system: Values can be shareable (freely duplicated, and memory managed) or linear (manually managed with move-copy semantics).
• Type-level programming: its type inference engine works with SMT solvers following the Liquid types paradigm. A rudimentary solver for the first-order theory of uninterpreted symbols is available to deal with user-defined sorts and symbols.
• (Defunctionalized-)continuation-passing-style: Contexts of evaluations are first-class data structures, and the analysis algorithms developed within AARA extend to those structures as well. Compared to previous AARA implementations, this allows for a streamlined type system that doesn’t have to track evaluation contexts in a ad-hoc manner.