Adventures in time and space

Norman Danner, James S. Royer

Research output: Chapter in Book/Entry/PoemConference contribution

3 Scopus citations


This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR1, has its first-order programs characterize the poly-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR1-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 poly-time. The time-restricting part is an affine version of Barber and Plotkin's DELL. Two semantics are constructed for ATR1. The first is a pruning of the naïve denotational semantics for ATR1. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR1 's time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR1 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.

Original languageEnglish (US)
Title of host publicationConference Record of POPL 2006
Subtitle of host publication33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery (ACM)
Number of pages12
ISBN (Print)1595930272, 9781595930279
StatePublished - 2006
Event33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'06 - Charleston, SC, United States
Duration: Jan 11 2006Jan 13 2006

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566


Conference33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'06
Country/TerritoryUnited States
CityCharleston, SC


  • Languages
  • Performance
  • Theory

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Adventures in time and space'. Together they form a unique fingerprint.

Cite this