一句话：提出带 oracle 调用的命令式语言与可判定层级类型系统，刻画基本可行泛函 BFF2。
基本可行泛函 BFF2 是多项式时间可计算函数类 FP 的二阶对应物，但已有刻画均未给出带类型系统且能保证该复杂度界的编程语言。本文提出一种带 oracle 调用的命令式编程语言，并设计基于 tier（层级）的类型系统，其类型推断是可判定的。作者证明该语言可精确刻画 BFF2，从而将高阶复杂度与编程理论联系起来。类型推断算法复杂度仅为程序规模的三次方，与既有方法的高不可解性形成对比，且不会过强限制语言表达能力。
The class of Basic Feasible Functionals BFF2 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 BFF2 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 restrain strongly the expressive power of the language.
@inproceedings{paperbot5536,
title = {A tier-based typed programming language characterizing Feasible Functionals},
author = {Emmanuel Hainry and Bruce M. Kapron and Jean-Yves Marion and Romain Péchoux},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394768}
}