A List of Papers on
Computational Complexity at Higher Types
and Related Topics
Version 2.0 – 29 July 1999
with sporadic updates since then
(Version 3 will be out one of these days.)
The following was originally built from the list of papers for
my Spring 97 course
Computation and Complexity at Higher Types. It is
incomplete, out of date, biased towards my interests, and the
categories & categorization are rather arbitary, but the list
may still be of use.

R. Gandy and J. Hyland,
Computable and recursively countable functions of higher type,
in Logic Colloquium 76,
NorthHolland
(1977)
407438.

This covers highertype computability.

S. Cook,
Computability and complexity of higher type functions,
in
Logic from Computer Science
(Y.N. Moschovakis, ed.),
SpringerVerlag
(1991)
5172.

This covers highertype computing and complexity and
contains some interesting original results, e.g.,
the quasilinear ordering functional.
A reasonable starting point for learning about
higher types and complexity.

J. Longley,
Notions of computability at higher types, I,
to appear in
Logic Colloquium 2000

A very nice historical survey.
See John Longley's
home page for the current drafts of Parts II and III.
A very good starting point for learning about higher types.

R. Irwin, B. Kapron, and J. Royer,
On Characterizations of the Basic Feasible Functionals, Part I
Journal of Functional Programming 11 (2001) 117153.

Roughly the first half of this is a survey of
complexity at higher types mainly focusing on type level 2.

R. Irwin, B. Kapron, and J. Royer,
On Characterizations of the Basic Feasible Functionals, Part II

The beginning of this paper has a brief survey of
complexity at higher types at type levels 3 and above.

S. Buss,
The Polynomial Hierarchy and Intuitionistic Bounded Arithmetic,
In
Structure in Complexity Theory,
SpringerVerlag
(1986)
77103.

Buss introduces a class of ``polynomialtime'' functionals
at all simple types as realizers for IS_{2}^{1},
his intuitionistic theory of bounded arithmetic. This
roughly parallels Gödel's use of primitive recursive
functionals in the Dialectica paper.

R. Constable,
Type two computational complexity,
in
Proc. of the Fifth Ann. ACM Symp. on Theory of Computing
(1973)
108121.

As far as I can tell this is the first paper to consider the
question of the computational complexity of functionals and
operators (as opposed to using functionals and operators as tools).

R. Daley and C. Smith,
On the Complexity of Inductive Inference,
Information and Control 69
(1986)
1240.

This concerns the computational complexity of limiting functionals
as used in learning theory.

K. Gödel,
Über eine bisher noch nicht benützte Erweiterung
des finiten,
in Dialectica
(1958)
280287. Available in English as:
K. Gödel,
On a hitherto unutilized extension of the finitary standpoint,
in Kurt Gödel: Collected Works, Volume II,
S. Feferman, J. Dawson, S. Kleene,
G. Moore, R. Solovay, and J. van Heijenoort (eds.),
Oxford University Press (1990) 241251.

Gödel Uses highertype primitive recursive functionals to
give a relative consistency proof for Heyting Arithmetic.

D. Hilbert,
Über das unendliche,
Mathematische Annalen 95
(1925)
161190. Available in English as:
D. Hilbert,
On the infinite,
in
From Frege to Gödel: A source book in mathematical logic,
18791931,
(J. van Heijenoort, ed.),
Harvard University Press
(1967)
367392.

In the course of his work on proof theory,
Hilbert uses a highertype primitive recursive
functional to define a variant of Ackerman's function.
This is one of the earliest uses of subrecursive highertype
recursion.
I have been told that C.S. Peirce's work on his Calculus of
Relations (the first version of which was published in 1870)
may well contain other examples.

K. Mehlhorn,
Polynomial and Abstract Subrecursive Classes,
Journal of Computer and Systems Sciences 12
(1976)
147178.

This was a follow up of some of the questions posed
by the 1973 Constable paper.

H. Schwichtenberg,
Functions definable in the simplytyped lambda calculus,
Arch. Math Logik 17
(1976)
113114.

This paper shows that the functions definable over the Church
numerals in the simply typed lambda calculus are precisely
the extended polynomial functions;
these are roughly the polynomials closed up under
a conditional operator.
Studies of the Basic Feasible Functionals
and Related Classes

P. Clote,
A note on the relation between polynomial time
functionals and Constable's class K, in
Proceedings of the Conference for Computer Science Logic '95,
LNCS 1092, SpringerVerlag (1996).

S. Cook and B. Kapron,
Characterizations of the basic feasible functions of finite type,
in
Feasible Mathematics:
A Mathematical Sciences Institute Workshop,
(S. Buss and P. Scott, eds.),
Birkhäuser
(1990)
7195.

Contains several programming formalism characterizations
of the type2 BFFs and shows that the type2 class studied
by Mehlhorn corresponds to the type2 BFFs.

S. Cook and A. Urquhart,
Functional Interpretations of Feasibly Constructive Arithmetic,
Annals of Pure and Applied Logic 63
(1993)
103200.

The first place the BFFs at all simple types appear.
The paper follows up some problems raised by Buss's paper.
Cook and Urquhart set out to develop an alternative class of
realizers for IS_{2}^{1} than
the ones used by Buss. The goal was to
present the result as a feasible variant of Gödel's
Dialectica interpretation of Heyting Arithmetic.
They introduced a formal system PV^{omega}
in which the terms consist of simply typed
lambdaexpressions built from numeric constants, function
constants for each polynomialtime computable function,
variables of all finite types,
and a type2 recursor that corresponds to Cobham's
limited recursion on notation.

R. Irwin, B. Kapron, and J. Royer,
On Characterizations of the Basic Feasible Functionals, Part I
(draft), 1999, to appear in the Journal of Functional
Programming.

This paper builds on the BellantoniCook and Leivant
characterizations of Ptime to obtain a kind of typetheoretic
characterization the type2 basic feasible functionals.
The first part contains a brief, but chatty, survey of
the prior work on the BFFs.

R. Irwin, B. Kapron, and J. Royer,
On Characterizations of the Basic Feasible Functionals, Part II

This concerns characterizations of the basic feasible
functionals as typelevel three and above. In
contrast to Part I, in which the focus was on types, the focus
here is on semantics. Be warned that this is a big,
complex paper that clarifies some mysteries and raises
some others.

B. Kapron and S. Cook,
A new characterization of type 2 feasibility,
SIAM Journal on Computing 25 (1996)
117132.

This contains the machine characterization of the type2
Basic Feasible Functionals  a very pretty result, but a
not so pretty proof.

B. Kapron,
Feasible Computation in Higher Types,
Ph.D. Thesis,
Department of Computer Science, University of Toronto,
1991.

B. Kapron,
Feasibly continuous typetwo functionals (1998),
to appear in Computational Complexity.
 C.C. Li and J. Royer
On Type2 Complexity Classes (Preliminary version) (draft),
presented at ICC'00.

There is currently no satisfactory
general notion of what a highertype complexity class should be.
In this paper we propose one such notion for type2 functionals
and begin an investigation of its properties.

E. Pezzoli,
On the computational complexity of type two functionals,
Proceedings of the Conference for Computer Science Logic '97,
LNCS 1414, SpringerVerlag (1998) 373388.

This is a continuation of Seth's work ``natural properties''
(my bad terminology, not theirs) that may characterize the
intuitively feasible type2 functionals. She shows that
the set of properties considered in Seth (1993) fail to
characterize the type2 BFFs and proposes a set of her own
that do indeed yield the characterization.

J. Royer,
Semantics vs. syntax vs. computations:
Machine models for type2 polynomialtime bounded functionals,
J. Comput. and Syst. Science
54 (1997) 424436.

A fairly natural direct analogue of KreiselLacombeSchoenfield
Theorem for type2 feasible functionals is shown to involve
complexitytheoretic conundrums. E.g., if this direct analogue
holds, then P differs from NP. A weaker ``feasible'' analogue
of KLS  in which "computing over syntax" is
replaced by "computing over computations (of programs)" 
is shown to hold.

J. Royer,
On the Computational Complexity of Longley's H Functional,
to appear in Theoretical Computer Science,
presented at ICC'00.

The sequentially realizable functionals (denoted SR)
is a class of ``sequentially computable'' highertype functionals
that include the PCFcomputable functionals along with elements
that are not Scottcontinuous. SR has very strong and
natural mathematical properties.
Longley exhibited a functional H in SR with the property that
if one adds H to the language PCF, then the resulting language,
PCF+H, computes exactly SR. Longley hesitated to recommend
PCF+H as the basis of a practical programming language as
the only known ways of computing H seemed to involve high
computational complexity.
This paper shows that if P is different from NP, then the
computational complexity of H (and of similar SRfunctionals)
is inherently infeasible.

A. Seth,
There is No Recursive Axiomatization for Feasible Functionals
of Type 2,
Seventh Annual IEEE Symposium on Logic in Computer Science
(1992)
286295.

A. Seth,
Some Desirable Conditions for Feasible Functions of Type 2,
Eighth Annual IEEE Symposium on Logic in Computer Science
(1993)
320331.

A. Seth,
Turing Machine Characterizations of Feasible Functionals
of All Finite Types,
in
Feasible Mathematics II,
Birkhäuser
(1995)
407428.

This contains an extension of the KapronCook
type2 machine characterization to all simple types.

A. Seth,
Complexity Theory of Higher Type Functionals,
Ph.D. Thesis,
University of Bombay,
1994.

This contains the matterial of the previous three
papers and more.
Characterizing Complexity Classes via
Categorical Constructs, LambdaCalculi, Logics, and, most especially, Types
There is too much recent work here for a comprehensive list.
So, just
some of the earlier papers are listed below. See
for a recent survey.
Also see
the home page of the International Workshop on Implicit
Computational Complexity, a continuing series of workshops on this
and related topics.

Andrea Asperti,
Light Affine Logic,
Proceedings of LICS '98,
IEEECS (1998).

S. Bellantoni,
Predicative recursion and computational complexity,
Ph.D. Thesis, University of Toronto,
published as University of Toronto, Computer Science Department
Technical Report 264/92 (1992).

S. Bellantoni and S. Cook,
A new recursiontheoretic characterization of the polytime functions,
Computational Complexity 2
(1992)
97110.

V.H. Caeserio,
Equations for Defining Polytime Functions,
Ph.D. Thesis, Univ. of Oslo, 1997.

P. Clote,
A safe recursion scheme for exponential time,
Boston College Computer Science Department Technical Report.

J.Y. Girard and A. Scedrov and P.J. Scott,
Bounded Linear Logic: A Modular Approach to Polynomial
Time Computability,
Theoretical Computer Science 97
(1992)
166.

J.Y. Girard,
Light Linear Logic,
Information and Computation 143
(1998) 175204.

A. Goerdt,
Characterizing Complexity Classes by HigherType
Primitive Recursive Definitions,
Theoretical Computer Science 100 (1992) 4566.

A. Goerdt and H. Seidl,
Characterizing Complexity Classes by HigherType
Primitive Recursive Definitions, Part II,
in
Aspects and Prospects of Theoretical Computer Science,
LNCS 464, J. Dassow and J. Kelemen (Eds.), SpringerVerlag (1990)
148158.

A. Goerdt,
Characterizing Complexity Classes by General Recursive
Definitions in Higher Types,
Information and Computation 101 (1992) 202218.

D. Leivant,
Ramified Recurrence and Computational Complexity I:
Word Recurrence and Polytime,
in
Feasible Mathematics II,
(P. Clote and J. Remmel, eds.)
Birkhäuser
(1995)
320343.

D. Leivant,
Predicative Recurrence in Finite Types,
in
Logical Foundations of Computer Science, Third International
Symposium, (A. Nerode, Yu. Matiyasevich, eds.),
Lecture Notes in Computer Science 813, SpringerVerlag
(1994)
227240.

J. Otto,
Complexity Doctrines,
Ph.D. thesis, McGill University, 1995.
Using Types to Build HigherType Functionals over
PolynomialTime

S. Bellantoni, K.H. Niggl, and H. Schwichtenberg,
Higher Type Recursion, Ramification and Polynomial Time,
to appear in Annals of Pure and Applied Logic.

M. Hofmann,
An application of categorytheoretic semantics to the
characterisation of complexity classes using higherorder
function algebras,
Bulletin of Symbolic Logic 3 (1997)
469486.

M. Hofmann,
Type systems for polynomialtime computation,
Habilitation thesis. Darmstadt, 1999.
Appears as LFCS Technical Report ECSLFCS99406.

M. Hofmann,
Linear types and nonsizeincreasing polynomial time computation,
in the Proceedings of the 1999 IEEE Conference on Logic in Computer
Science (1999).

J.C. Mitchell, M. Mitchell, and A. Scedrov,
A linguistic characterization of bounded oracle computation
and probabilistic polynomial time,
in the Proceedings of the 1998 IEEE Symposium on the Foundations of
Computer Science (1998) 725733.

E. Rose,
Linear Time Hierarchies for a Functional Language Machine Model,
to appear in
Science of Computer Programming.
Other Papers of Interest

D. Gurr,
Semantic Frameworks for Complexity,
Ph.D. Thesis, University of Edinburgh,
1990.

H. Mairson,
A Simple Proof of a Theorem of Statman,
Theoretical Computer Science 103
(1992)
387394.

This result is a nice contrast to the one of
Schwichtenberg's 1976 paper listed above.

H. Schwichtenberg,
Density and choice for total continuous functionals,
in
Kreiseliana
(P. Odifreddi, ed.),
A.K. Peters
(1996)
335362.

H. Schwichtenberg,
Type Theory,
lecture notes from a course given at Universität München,
1994.

D. Scott,
A typetheoretical alternative to ISWIM, CUCH, and OWHY,
Theoretical Computer Science 121
(1993)
411440,
Originally written in 1969.

M. Townsend,
Complexity for Type2 Relations,
Nortre Dame Journal of Formal Logic 31
(1990)
241262.

T. Yamakami,
Feasible Computability and Resource Bounded Topology,
Information and Computation 116
(1995)
214230.

This is a follow up to Townsend's paper.

R. Hindley,
Basic Simple Type Theory,
Cambridge,
1997.

N. Jones,
Computability and Complexity from a Programming Perspective,
MIT Press,
1997.

P. Odifreddi,
Classical Recursion Theory, Vol. I
North Holland,
1989.

P. Odifreddi,
Classical Recursion Theory, Vol. II
North Holland,
1999.

C. Okasaki,
Purely Functional Data Structures,
Cambridge,
1998.

C. Papadimitriou,
Computational Complexity,
AddisonWesley,
1994.

H. Rogers,
Theory of Recursive Functions and Effective Computability,
McGrawHill,
1969.

J. Royer and J. Case,
Subrecursive Programming Systems: Complexity & Succinctness,
Birkhäuser,
1994.

DIMACS Workshop on Computational
Complexity and Programming Languages, Rutgers University, 1996.
See the
Workshop Report.

Programs: Improvements, Complexity, and Meanings;
Schloß Dagstuhl;
Wadern, Germany, 812 June 1998.

The Implicit Computational Complexity in Programming Language Design
and Methodology Workshop, Baltimore, Maryland, USA,
26 September 1998.

Implicit Computational Complexity Workshop
Trento, Italy, 30 June  1 July, 1999.

Implicit Computational Complexity2000
2930 June 2000, UC/SantaBarbara.
Dante and Beatrice contemplate higher types
and computational complexity
(notice all the bigOs)
An example of downward tier coercion
(see the Irwin, Kapron, and Royer papers)
More Dore Illustrations for Dante's Comedy
Acknowledgement and Disclaimer
This material is based in part upon work supported by the National
Science Foundation under Grants CCR9522987 and CCR0098198.
Any opinions, findings, and conclusions or recommendations expressed
in this material are those of the author and do not necessarily
reflect the views of the National Science Foundation.
http://www.cis.syr.edu/~royer/
Last systematic modification: August 1999