From bounded affine types to automatic timing analysis

TL;DR

This paper introduces an affine bounded linear type system for resource modeling in semirings, providing a general type-inference method and semantics, with applications to resource-sensitive compilation and timing analysis in functional programming.

Contribution

It generalizes existing type systems by incorporating affine bounded linear types with a semiring-based resource model and offers a type inference procedure and categorical semantics.

Findings

Developed a general type-inference procedure based on semiring decision procedures.

Provided a categorical semantics for the affine bounded linear type system.

Applied the framework to timing analysis in higher-order functional programming with local store.

Abstract

Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce an affine bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This is a very useful type-theoretic and denotational framework for many applications to resource-sensitive compilation, and it represents a generalization of several existing type systems. As a non-trivial instance, motivated by our ongoing work on hardware compilation, we present a complex new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.