A unifying framework for continuity and complexity in higher types

Research output: Contribution to journalArticle

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 (Nat → Nat) → Nat in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.

Original languageEnglish
Pages (from-to)17:1-17:28
JournalLogical Methods in Computer Science
Volume16
Issue number3
DOIs
Publication statusPublished - 9 Sep 2020

Keywords

  • Bar recursion
  • Denotational semantics
  • Functional languages
  • Logical relations

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this