T. Arai & G. Moser (2005):
Proofs of Termination of Rewrite Systems for Polytime Functions.
In: Proceedings of the 25th FSTTCS,
LNCS 3821,
pp. 529–540,
doi:10.1007/11590156_43.
M. Avanzini & U. Dal Lago (2015):
On Sharing, Memoization, and Polynomial Time.
In: Proceedings of the 32nd STACS,
pp. 62–75,
doi:10.4230/LIPIcs.STACS.2015.62.
M. Avanzini, N. Eguchi & G. Moser (2011):
A Path Order for Rewrite Systems that Compute Exponential Time Functions.
In: Proceedings of the 22nd RTA,
LIPIcs 10,
pp. 123–138,
doi:10.4230/LIPIcs.RTA.2011.123.
M. Avanzini, N. Eguchi & G. Moser (2012):
A New Order-theoretic Characterisation of the Polytime Computable Functions.
In: Proceedings of the 10th APLAS,
LNCS 7705,
pp. 280–295,
doi:10.1007/978-3-642-35182-2_20.
H. P. Barendregt, M. C. J. D. van Eekelen, J. R. W. Glauert, R. Kennaway, M. J. Plasmeijer & M. R. Sleep (1987):
Term Graph Rewriting.
In: Parallel Architectures and Languages Europe, Volume II 259,
pp. 141–158,
doi:10.1007/3-540-17945-3_8.
S. Bellantoni & S. A. Cook (1992):
A New Recursion-theoretic Characterization of the Polytime Functions.
Computational Complexity 2(2),
pp. 97–110,
doi:10.1007/BF01201998.
G. Bonfante, A. Cichon, J.-Y. Marion & H. Touzet (2001):
Algorithms with Polynomial Interpretation Termination Proof.
J. Funct. Program. 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: The 4th Andrei Ershov Memorial Conference, Revised Papers,
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.
Theor. Comput. Sci. 412(25),
pp. 2776–2796,
doi:10.1016/j.tcs.2011.02.007.
U. Dal Lago, S. Martini & M. Zorzi (2010):
General Ramified Recurrence is Sound for Polynomial Time.
In: Patrick Baillot: Proceedings DICE 2010,
pp. 47–62,
doi:10.4204/EPTCS.23.4.
N. Eguchi (2014):
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion.
Available at http://arxiv.org/abs/1404.6196.
Technical report.
W. G. Handley & S. S. Wainer (1999):
Complexity of Primitive Recursion.
In: U. Berger & H. Schwichtenberg: Computational Logic,
NATO ASI Series F: Computer and Systems Science 165.
Springer,
pp. 273–300,
doi:10.1007/978-3-642-58622-4_8.
D. Leivant (1995):
Ramified Recurrence and Computational Complexity I: Word Recurrence and Poly-time.
In: Peter Clote & Jeffrey B. Remmel: Feasible Mathematics II, Progress in Computer Science and Applied Logic 13.
Birkhäuser Boston,
pp. 320–343,
doi:10.1007/978-1-4612-2566-9_11.
D. Leivant & J.-Y. Marion (1994):
Ramified Recurrence and Computational Complexity II: Substitution and Poly-Space.
In: The 8th CSL, Selected Papers,
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.
A. Middeldorp, H. Ohsaki & H. Zantema (1996):
Transforming Termination by Self-Labeling.
In: Proceedings of the 13th CADE,
LNCS 1104,
pp. 373–387,
doi:10.1007/3-540-61511-3_101.
eptcs@eptcs.org