Alarcón, B., Gutiérrez, R., & Lucas, S. (2010). Context-sensitive dependency pairs. Information and Computation, 208(8), 922-968. doi:10.1016/j.ic.2010.03.003
Alpuente, M., Escobar, S., & Lucas, S. (2004). Correct and Complete (Positive) Strategy Annotations for OBJ. Electronic Notes in Theoretical Computer Science, 71, 70-89. doi:10.1016/s1571-0661(05)82529-0
Andrianarivelo, N., & Réty, P. (2015). Over-Approximating Terms Reachable by Context-Sensitive Rewriting. Reachability Problems, 128-139. doi:10.1007/978-3-319-24537-9_12
[+]
Alarcón, B., Gutiérrez, R., & Lucas, S. (2010). Context-sensitive dependency pairs. Information and Computation, 208(8), 922-968. doi:10.1016/j.ic.2010.03.003
Alpuente, M., Escobar, S., & Lucas, S. (2004). Correct and Complete (Positive) Strategy Annotations for OBJ. Electronic Notes in Theoretical Computer Science, 71, 70-89. doi:10.1016/s1571-0661(05)82529-0
Andrianarivelo, N., & Réty, P. (2015). Over-Approximating Terms Reachable by Context-Sensitive Rewriting. Reachability Problems, 128-139. doi:10.1007/978-3-319-24537-9_12
Borralleras, C., Ferreira, M., & Rubio, A. (2000). Complete Monotonic Semantic Path Orderings. Lecture Notes in Computer Science, 346-364. doi:10.1007/10721959_27
Borralleras, C., Lucas, S., & Rubio, A. (2002). Recursive Path Orderings Can Be Context-Sensitive. Lecture Notes in Computer Science, 314-331. doi:10.1007/3-540-45620-1_27
Gérard Boudol. 1985. Computational semantics of term rewriting systems. Algebr. Methods Semant. (1985) 169--236. Gérard Boudol. 1985. Computational semantics of term rewriting systems. Algebr. Methods Semant. (1985) 169--236.
Bruni, R., & Meseguer, J. (2006). Semantic foundations for generalized rewrite theories. Theoretical Computer Science, 360(1-3), 386-414. doi:10.1016/j.tcs.2006.04.012
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı́-Oliet, N., Meseguer, J., & Quesada, J. F. (2002). Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285(2), 187-243. doi:10.1016/s0304-3975(01)00359-0
Clavel, M., Eker, S., Lincoln, P., & Meseguer, J. (1996). Principles of Maude. Electronic Notes in Theoretical Computer Science, 4, 65-89. doi:10.1016/s1571-0661(04)00034-9
Courcelle, B. (1983). Fundamental properties of infinite trees. Theoretical Computer Science, 25(2), 95-169. doi:10.1016/0304-3975(83)90059-2
Dershowitz, N. (1979). A note on simplification orderings. Information Processing Letters, 9(5), 212-215. doi:10.1016/0020-0190(79)90071-1
Dershowitz, N., Kaplan, S., & Plaisted, D. A. (1991). Rewrite, rewrite, rewrite, rewrite, rewrite, …. Theoretical Computer Science, 83(1), 71-96. doi:10.1016/0304-3975(91)90040-9
Eker, S. (1998). Term Rewriting with Operator Evaluation Strategies. Electronic Notes in Theoretical Computer Science, 15, 311-330. doi:10.1016/s1571-0661(05)80019-2
Jörg Endrullis . 2009. Jambox. ( 2009 ). Retrieved from http://joerg.endrullis.de/jambox.html. Jörg Endrullis. 2009. Jambox. (2009). Retrieved from http://joerg.endrullis.de/jambox.html.
Endrullis, J., & Hendriks, D. (2011). Lazy productivity via termination. Theoretical Computer Science, 412(28), 3203-3225. doi:10.1016/j.tcs.2011.03.024
Futatsugi, K., Goguen, J. A., Jouannaud, J.-P., & Meseguer, J. (1985). Principles of OBJ2. Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL ’85. doi:10.1145/318593.318610
Futatsugi, K., & Nakagawa, A. (s. f.). An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks. Proceedings First IEEE International Conference on Formal Engineering Methods. doi:10.1109/icfem.1997.630424
Giesl, J. (2001). Journal of Automated Reasoning, 26(1), 1-49. doi:10.1023/a:1006408829523
GIESL, J., & MIDDELDORP, A. (2004). Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming, 14(4), 379-427. doi:10.1017/s0956796803004945
Jürgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics Held as Part of ETAPS’19 Part III Dirk Beyer Marieke Huisman Fabrice Kordon and Bernhard Steffen (Eds.) Lecture Notes in Computer Science Vol. 11429. Springer 156--166. DOI:https://doi.org/10.1007/978-3-030-17502-3_10 Jürgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics Held as Part of ETAPS’19 Part III Dirk Beyer Marieke Huisman Fabrice Kordon and Bernhard Steffen (Eds.) Lecture Notes in Computer Science Vol. 11429. Springer 156--166. DOI:https://doi.org/10.1007/978-3-030-17502-3_10
Giesl, J., Thiemann, R., Schneider-Kamp, P., & Falke, S. (2007). Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning, 37(3), 155-203. doi:10.1007/s10817-006-9057-7
Goguen, J., & Malcolm, G. (Eds.). (2000). Software Engineering with OBJ. Advances in Formal Methods. doi:10.1007/978-1-4757-6541-0
Gramlich, B., & Lucas, S. (2002). Simple termination of context-sensitive rewriting. Proceedings of the 2002 ACM SIGPLAN workshop on Rule-based programming - RULE ’02. doi:10.1145/570186.570189
Gramlich, B., & Lucas, S. (2006). Generalizing Newman’s Lemma for Left-Linear Rewrite Systems. Term Rewriting and Applications, 66-80. doi:10.1007/11805618_6
Gutiérrez, R., & Lucas, S. (2010). Proving Termination in the Context-Sensitive Dependency Pair Framework. Lecture Notes in Computer Science, 18-34. doi:10.1007/978-3-642-16310-4_3
Raúl Gutiérrez and Salvador Lucas. 2015. Function calls at frozen positions in termination of context-sensitive rewriting See Martí-Oliet et al. [2015] 311--330. DOI:https://doi.org/10.1007/978-3-319-23165-5_15 Raúl Gutiérrez and Salvador Lucas. 2015. Function calls at frozen positions in termination of context-sensitive rewriting See Martí-Oliet et al. [2015] 311--330. DOI:https://doi.org/10.1007/978-3-319-23165-5_15
Gutiérrez, R., & Lucas, S. (2020). Automatically Proving and Disproving Feasibility Conditions. Lecture Notes in Computer Science, 416-435. doi:10.1007/978-3-030-51054-1_27
Hirokawa, N., & Moser, G. (2014). Automated Complexity Analysis Based on Context-Sensitive Rewriting. Rewriting and Typed Lambda Calculi, 257-271. doi:10.1007/978-3-319-08918-8_18
Hirokawa, N., Nagele, J., & Middeldorp, A. (2018). Cops and CoCoWeb: Infrastructure for Confluence Tools. Lecture Notes in Computer Science, 346-353. doi:10.1007/978-3-319-94205-6_23
Hudak, P. (1989). Conception, evolution, and application of functional programming languages. ACM Computing Surveys, 21(3), 359-411. doi:10.1145/72551.72554
Hudak, P., Peyton Jones, S., Wadler, P., Boutel, B., Fairbairn, J., Fasel, J., … Peterson, J. (1992). Report on the programming language Haskell. ACM SIGPLAN Notices, 27(5), 1-164. doi:10.1145/130697.130699
J. F. Th. Kamperman and H. R. Walters . 1995 . Lazy rewriting and eager machinery. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA’95) Jieh Hsiang (Ed.) Lecture Notes in Computer Science Vol. 914 . Springer 147--162. DOI:https://doi.org/10.1007/3-540-59200-8_54 J. F. Th. Kamperman and H. R. Walters. 1995. Lazy rewriting and eager machinery. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA’95) Jieh Hsiang (Ed.) Lecture Notes in Computer Science Vol. 914. Springer 147--162. DOI:https://doi.org/10.1007/3-540-59200-8_54
Kennaway, R., Klop, J. W., Sleep, R., & Devries, F. J. (1995). Transfinite Reductions in Orthogonal Term Rewriting Systems. Information and Computation, 119(1), 18-38. doi:10.1006/inco.1995.1075
Kojima, Y., & Sakai, M. (s. f.). Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems. Lecture Notes in Computer Science, 187-201. doi:10.1007/978-3-540-70590-1_13
Kojima, Y., Sakai, M., Nishida, N., Kusakari, K., & Sakabe, T. (2011). Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems. IPSJ Online Transactions, 4, 193-216. doi:10.2197/ipsjtrans.4.193
Lucas, S. (2001). Transfinite Rewriting Semantics for Term Rewriting Systems. Lecture Notes in Computer Science, 216-230. doi:10.1007/3-540-45127-7_17
Lucas, S. (2002). Context-Sensitive Rewriting Strategies. Information and Computation, 178(1), 294-343. doi:10.1016/s0890-5401(02)93176-7
Lucas, S. (2002). Termination of (Canonical) Context-Sensitive Rewriting. Lecture Notes in Computer Science, 296-310. doi:10.1007/3-540-45610-4_21
Lucas, S. (2006). Proving termination of context-sensitive rewriting by transformation. Information and Computation, 204(12), 1782-1846. doi:10.1016/j.ic.2006.07.001
Salvador Lucas. 2020. Applications of context-sensitive rewriting. (submitted). Salvador Lucas. 2020. Applications of context-sensitive rewriting. (submitted).
Maranget, L. (1991). Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems. Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’91. doi:10.1145/99583.99618
McCarthy, J. (1960). Recursive functions of symbolic expressions and their computation by machine, Part I. Communications of the ACM, 3(4), 184-195. doi:10.1145/367177.367199
Meseguer, J. (2012). Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming, 81(7-8), 721-781. doi:10.1016/j.jlap.2012.06.003
Middeldorp, A. (1997). Call by need computations to root-stable form. Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’97. doi:10.1145/263699.263711
Nagele, J., Felgenhauer, B., & Middeldorp, A. (2017). CSI: New Evidence – A Progress Report. Lecture Notes in Computer Science, 385-397. doi:10.1007/978-3-319-63046-5_24
Nagele, J., Thiemann, R., & Winkler, S. (2014). Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. Lecture Notes in Computer Science, 216-232. doi:10.1007/978-3-319-12154-3_14
Dag Prawitz. 1965. Natural Deduction. A Proof Theoretical Study. Almqvist 8 Wiksell. Dag Prawitz. 1965. Natural Deduction. A Proof Theoretical Study. Almqvist 8 Wiksell.
Raffelsieper, M., & Zantema, H. (2009). A Transformational Approach to Prove Outermost Termination Automatically. Electronic Notes in Theoretical Computer Science, 237, 3-21. doi:10.1016/j.entcs.2009.03.032
Rapp, F., & Middeldorp, A. (2018). FORT 2.0. Lecture Notes in Computer Science, 81-88. doi:10.1007/978-3-319-94205-6_6
Schernhammer, F., & Gramlich, B. (2009). VMTL–A Modular Termination Laboratory. Lecture Notes in Computer Science, 285-294. doi:10.1007/978-3-642-02348-4_20
Thiemann, R., & Sternagel, C. (2009). Certification of Termination Proofs Using CeTA. Theorem Proving in Higher Order Logics, 452-468. doi:10.1007/978-3-642-03359-9_31
Thiemann, R., & Sternagel, C. (2009). Loops under Strategies. Lecture Notes in Computer Science, 17-31. doi:10.1007/978-3-642-02348-4_2
Uchiyama, K., Sakai, M., & Sakabe, T. (2008). Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems. Electronic Notes in Theoretical Computer Science, 204, 21-34. doi:10.1016/j.entcs.2008.03.051
Zantema, H. (1997). Termination of context-sensitive rewriting. Lecture Notes in Computer Science, 172-186. doi:10.1007/3-540-62950-5_69
[-]