# A unifying framework for continuity and complexity in higher types

## TL;DR

This paper introduces a unified framework for analyzing higher-order computation concepts like termination, continuity, and complexity in functional languages, providing new methods for extracting moduli and characterizing complexity.

## Contribution

It develops a parametrised monadic translation that unifies various notions in higher types and offers concrete instantiations for analyzing continuity and complexity.

## Key findings

- Unified scheme for higher-order notions
- Method for extracting moduli of continuity
- Characterization of bar recursion complexity

## Abstract

We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main goal is to provide a unifying scheme which brings together several concepts which are often treated separately in the literature. However, as a by-product, we also obtain (i) a method for extracting moduli of continuity for closed functionals of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ definable in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.