@article(BeckB14,
 author       = {A. Beckmann and S.R. Buss},
 year         = {2014},
 title        = {Improved Witnessing and Local Improvement Principles for Second-order Bounded Arithmetic},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {15},
 number       = {1},
 pages        = {2},
 doi          = {10.1145/2559950},
)
@article(BCMT01,
 author       = {G. Bonfante and A. Cichon and J.-Y. Marion and H. Touzet},
 year         = {2001},
 title        = {Algorithms with Polynomial Interpretation Termination Proof},
 journal      = {Journal of Functional Programming},
 volume       = {11},
 number       = {1},
 pages        = {33--53},
 doi          = {10.1017/S0956796800003877},
)
@inproceedings(BMM01,
 author       = {G. Bonfante and J.-Y. Marion and J.-Y. Moyen},
 year         = {2001},
 title        = {{On Lexicographic Termination Ordering with Space Bound Certifications}},
 booktitle    = {Perspectives of System Informatics},
 series       = {Lecture Notes in Computer Science},
 volume       = {2244},
 pages        = {482--493},
 doi          = {10.1007/3-540-45575-2\_46},
)
@article(BMM11,
 author       = {G. Bonfante and J.-Y. Marion and J.-Y. Moyen},
 year         = {2011},
 title        = {Quasi-interpretations A Way to Control Resources},
 journal      = {Theoretical Computer Science},
 volume       = {412},
 number       = {25},
 pages        = {2776--2796},
 doi          = {10.1016/j.tcs.2011.02.007},
)
@article(buch95,
 author       = {W. Buchholz},
 year         = {1995},
 title        = {Proof-theoretic Analysis of Termination Proofs},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {75},
 number       = {1--2},
 pages        = {57--65},
 doi          = {10.1016/0168-0072(94)00056-9},
)
@book(buss86,
 author       = {S.R. Buss},
 year         = {1986},
 title        = {Bounded Arithmetic},
 publisher    = {Bibliopolis, Napoli},
)
@incollection(buss98,
 author       = {S.R. Buss},
 year         = {1998},
 title        = {{First-Order Proof Theory of Arithmetic}},
 editor       = {S.R. Buss},
 booktitle    = {Handbook of Proof Theory},
 publisher    = {North Holland, Amsterdam},
 pages        = {79--147},
 doi          = {10.1016/S0049-237X(98)80017-7},
)
@article(Dershowitz82,
 author       = {N. Dershowitz},
 year         = {1982},
 title        = {{Orderings for Term-Rewriting Systems}},
 journal      = {Theoretical Computer Science},
 volume       = {17},
 pages        = {279--301},
 doi          = {10.1016/0304-3975(82)90026-3},
)
@incollection(Eguchi10,
 author       = {N. Eguchi},
 year         = {2010},
 title        = {A Term-rewriting Characterization of PSPACE},
 editor       = {T. Arai and C.T. Chong and R. Downey and J. Brendle and Q. Feng and H. Kikyo and H. Ono},
 booktitle    = {Proceedings of the 10th Asian Logic Conference 2008},
 publisher    = {World Scientific},
 pages        = {93--112},
 doi          = {10.1142/9789814293020\_0004},
)
@inproceedings(Hof90,
 author       = {D. Hofbauer},
 year         = {1990},
 title        = {Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths},
 booktitle    = {Proceedings of the 2nd International Conference on Algebraic and Logic Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {463},
 pages        = {347--358},
 doi          = {10.1007/3-540-53162-9\_50},
)
@book(Jones97,
 author       = {N.D. Jones},
 year         = {1997},
 title        = {Computability and Complexity - from a Programming Perspective},
 series       = {Foundations of Computing Series},
 publisher    = {MIT Press},
 doi          = {10.1007/978-94-010-0413-8\_4},
)
@inproceedings(JonesM86,
 author       = {N.D. Jones and A. Mycroft},
 year         = {1986},
 title        = {Data Flow Analysis of Applicative Programs Using Minimal Function Graphs},
 booktitle    = {Proceedings of the 13th ACM Symposium on Principles of Programming Languages},
 pages        = {296--306},
 doi          = {10.1145/512644.512672},
)
@unpublished(Kamin_Levy,
 author       = {S. Kamin and J.-J. L\'{e}vy},
 year         = {1980},
 title        = {Two Generalizations of the Recursive Path Ordering},
 note         = {Unpublished manuscript, University of Illinois},
)
@article(LM95,
 author       = {D. Leivant and J.-Y. Marion},
 year         = {1995},
 title        = {{Ramified Recurrence and Computational Complexity II: Substitution and Poly-space}},
 journal      = {Lecture Notes in Computer Science},
 volume       = {933},
 pages        = {486--500},
 doi          = {10.1007/BFb0022277},
)
@article(Marion03,
 author       = {J.-Y. Marion},
 year         = {2003},
 title        = {Analysing the Implicit Complexity of Programs},
 journal      = {Information and Computation},
 volume       = {183},
 number       = {1},
 pages        = {2--18},
 doi          = {10.1016/S0890-5401(03)00011-7},
)
@incollection(Oitavem01,
 author       = {I. Oitavem},
 year         = {2001},
 title        = {Implicit Characterizations of Pspace},
 booktitle    = {Proof Theory in Computer Science},
 series       = {Lecture Notes in Computer Science},
 volume       = {2183},
 publisher    = {Springer},
 pages        = {170--190},
 doi          = {10.1007/3-540-45504-3\_11},
)
@article(Oitavem02,
 author       = {I. Oitavem},
 year         = {2002},
 title        = {A Term Rewriting Characterization of the Functions Computable in Polynomial Space},
 journal      = {Archive for Mathematical Logic},
 volume       = {41},
 number       = {1},
 pages        = {35--47},
 doi          = {10.1007/s001530200002},
)
@article(Savitch70,
 author       = {W.J. Savitch},
 year         = {1970},
 title        = {Relationships Between Nondeterministic and Deterministic Tape Complexities},
 journal      = {Journal of Computer and System Sciences},
 volume       = {4},
 number       = {2},
 pages        = {177--192},
 doi          = {10.1016/S0022-0000(70)80006-X},
)
@book(SlonnegerK95,
 author       = {K. Slonneger and B.L. Kurtz},
 year         = {1995},
 title        = {Formal Syntax and Semantics of Programming Languages - A Laboratory Based Approach},
 publisher    = {Addison-Wesley},
)
@book(Terese,
 author       = {Terese},
 year         = {2003},
 title        = {Term Rewriting Systems},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 volume       = {55},
 publisher    = {Cambridge University Press},
)
@article(Thompson72,
 author       = {D.B. Thompson},
 year         = {1972},
 title        = {Subrecursiveness: Machine-Independent Notions of Computability in Restricted Time and Storage},
 journal      = {Mathematical Systems Theory},
 volume       = {6},
 number       = {1},
 pages        = {3--15},
 doi          = {10.1007/BF01706069},
)
@article(Weier95,
 author       = {A. Weiermann},
 year         = {1995},
 title        = {Termination Proofs for Term Rewriting Systems by Lexicographic Path Orderings Imply Multiply Recursive Derivation Lengths},
 journal      = {Theoretical Computer Science},
 volume       = {139},
 number       = {1{\&}2},
 pages        = {355--362},
 doi          = {10.1016/0304-3975(94)00135-6},
)
@book(Winskel93,
 author       = {G. Winskel},
 year         = {1993},
 title        = {The Formal Semantics of Programming Languages - An Introduction},
 series       = {Foundations of Computing Series},
 publisher    = {MIT Press},
)