Adventures in time and space

Abstract. This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR, has its first-order programs characterize the polynomial-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR-types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of polynomial-time. The time-restricting part is an affine version of Barber and Plotkin's DILL. Two semantics are constructed for ATR. The first is a pruning of the na?ive denotational semantics for ATR. This pruning removes certain functions that cause otherwise feasibl...

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Norman Danner, James S. Royer
• Keywords: Basic Feasible Functionals, Complexity-theoretically Motivated Type, Polynomial Time Bounds, POPL 2006, Programming Languages