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