[TYPES/announce] Paper Announcement: Adventures in Time and Space

[James S. Royer]

We would like to annouce the availability of a new paper:

TITLE: Adventures in Time and Space

AUTHORS: Norman Danner and James S. Royer

    This is the full version of our POPL'06 paper of the same name.

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
    naive denotational semantics for ATR.  This pruning removes
    certain functions that cause otherwise feasible forms of
    recursion to go wrong.  The second semantics is a model for
    ATR's time complexity relative to a certain abstract machine.
    This model provides a setting for complexity recurrences arising
    from ATR recursions, the solutions of which yield second-order
    polynomial time bounds.  The time-complexity semantics is also
    shown to be sound relative to the costs of interpretation on the
    abstract machine.

The paper is available as:
     ftp://ftp.cis.syr.edu/users/royer/ats.pdf
     ftp://ftp.cis.syr.edu/users/royer/ats.ps


Norman Danner and Jim Royer