Certifying and reasoning about cost annotations of functional programs

TL;DR

This paper introduces a labeling method for inserting cost annotations into higher-order functional programs, enabling certification of their correctness through compilation and reasoning within a higher-order Hoare logic framework.

Contribution

The paper presents a novel labeling technique for cost annotations that ensures correctness certification and facilitates reasoning in higher-order Hoare logic.

Findings

Cost annotations can be certified for correctness during compilation.

The method supports reasoning about costs in higher-order functional programs.

Framework integrates cost certification with standard compilation processes.

Abstract

We present a so-called labelling method to insert cost annotations in a higher-order functional program, to certify their correctness with respect to a standard compilation chain to assembly code including safe memory management, and to reason on them in a higher-order Hoare logic.