- -

Context-sensitive Rewriting

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Context-sensitive Rewriting

Mostrar el registro completo del ítem

Lucas Alba, S. (2020). Context-sensitive Rewriting. ACM Computing Surveys. 53(4):1-36. https://doi.org/10.1145/3397677

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/166526

Ficheros en el ítem

[Cerrado]
Nombre: Lucas - Context-s ...
Tamaño: 881.5Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor

Metadatos del ítem

Título: Context-sensitive Rewriting
Autor: Lucas Alba, Salvador
Entidad UPV: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Fecha difusión:
Resumen:
[EN] The appropriate selection of the arguments of functions that can be evaluated in function calls is often useful to improve efficiency, speed, termination behavior, and so on. This is essential, e.g., in the conditional ...[+]
Palabras clave: Programming languages , Term rewriting
Derechos de uso: Cerrado
Fuente:
ACM Computing Surveys. (issn: 0360-0300 )
DOI: 10.1145/3397677
Editorial:
Association for Computing Machinery
Versión del editor: https://doi.org/10.1145/3397677
Código del Proyecto:
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/
Agradecimientos:
Supported by the EU (FEDER) and projects RTI2018-094403-B-C32, PROMETEO/2019/098, and SP20180225.
Tipo: Artículo

References

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

[-]

recommendations

 

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro completo del ítem