A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations

Patrick Baillot, Ugo Dal Lago, Cynthia Kop +1

The class of type-two basic feasible functionals (${\mathtt{BFF}}_2$) is the analogue of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that c…