Sciweavers

POPL
2006
ACM

Adventures in time and space

14 years 3 months ago
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...
Norman Danner, James S. Royer
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Norman Danner, James S. Royer
Comments (0)