## Emmanuel Hainry ; Bruce M. Kapron ; Jean-Yves Marion ; Romain Péchoux - A tier-based typed programming language characterizing Feasible Functionals

lmcs:7216 - Logical Methods in Computer Science, February 24, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:33)2022
A tier-based typed programming language characterizing Feasible Functionals

Authors: Emmanuel Hainry ; Bruce M. Kapron ; Jean-Yves Marion ; Romain Péchoux

The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF$_2$ based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.

Volume: Volume 18, Issue 1
Published on: February 24, 2022
Accepted on: February 8, 2022
Submitted on: February 24, 2021
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages
Fundings :
Source : OpenAIRE Research Graph
• Funder: Natural Sciences and Engineering Research Council of Canada