On complexity bounds and confluence of parallel term rewriting. (English) Zbl 07929262
Summary: We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. Our approach to find lower bounds requires confluence of the parallel-innermost rewrite relation, thus we also provide effective sufficient criteria for proving confluence. The applicability and the precision of the method are demonstrated by the relatively light effort in extending the program analysis tool AProVE and by experiments on numerous benchmarks from the literature.
MSC:
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Baudon T, Fuhs C, Gonnord L. On Complexity Bounds and Confluence of Parallel Term Rewriting, 2024. URL https://arxiv.org/abs/2305.18250. |
| [2] | Baillot P, Ghyselen A. Types for Complexity of Parallel Computation in Pi-Calculus. In: Yoshida N (ed.), Programming Languages and Systems -30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 -April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science. Springer, 2021 pp. 59-86. URL https://doi.org/10.1007/978-3-030-72019-3_3. · Zbl 1473.68111 · doi:10.1007/978-3-030-72019-3_3 |
| [3] | Baillot P, Ghyselen A, Kobayashi N. Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. In: Haddad S, Varacca D (eds.), 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2021 pp. 34:1-34:22. URL https://doi.org/10.4230/LIPIcs. CONCUR.2021.34. · Zbl 07730636 · doi:10.4230/LIPIcs.CONCUR.2021.34 |
| [4] | Klemen M, López-García P, Gallagher JP, Morales JF, Hermenegildo MV. A General Framework for Static Cost Analysis of Parallel Logic Programs. In: Gabbrielli M (ed.), Logic-Based Program Synthesis and Transformation -29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8-10, 2019,. · Zbl 1502.68068 · doi:10.1007/978-3-030-45260-5_2 |
| [5] | Albert E, Correas J, Johnsen EB, Pun KI, Román-Díez G. Parallel Cost Analysis. ACM Trans. Comput. Logic, 2018. 19(4):31:1-31:37. URL https://doi.org/10.1145/3274278. · Zbl 1407.68062 · doi:10.1145/3274278 |
| [6] | Hoffmann J, Shao Z. Automatic Static Cost Analysis for Parallel Programs. In: Vitek J (ed.), Programming Languages and Systems -24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9032 of Lecture Notes in Computer Science. Springer, 2015 pp. 132-157. URL https://doi.org/10.1007/978-3-662-46669-8_6. · Zbl 1335.68056 · doi:10.1007/978-3-662-46669-8_6 |
| [7] | Das A, Hoffmann J, Pfenning F. Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang., 2018. 2(ICFP):91:1-91:30. URL https://doi.org/10.1145/3236786. · doi:10.1145/3236786 |
| [8] | Vuillemin J. Correct and Optimal Implementations of Recursion in a Simple Programming Language. J. Comput. Syst. Sci., 1974. 9(3):332-354. URL https://doi.org/10.1016/S0022-0000(74)80048-6. · doi:10.1016/S0022-0000(74)80048-6 |
| [9] | Fernández M, Godoy G, Rubio A. Orderings for Innermost Termination. In: Giesl J (ed.), Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science. Springer, 2005 pp. 17-31. URL https://doi.org/ 10.1007/978-3-540-32033-3_3. · Zbl 1078.68060 · doi:10.1007/978-3-540-32033-3_3 |
| [10] | Alias C, Fuhs C, Gonnord L. Estimation of Parallel Complexity with Rewriting Techniques. In: Proceedings of the 15th Workshop on Termination (WST 2016). 2016 pp. 2:1-2:5. URL https: //hal.archives-ouvertes.fr/hal-01345914. |
| [11] | van Eerd J, Groote JF, Hijma P, Martens J, Wijs A. Term Rewriting on GPUs. In: Hojjat H, Massink M (eds.), Fundamentals of Software Engineering -9th International Conference, FSEN 2021, Virtual Event, May 19-21, 2021,. · Zbl 1496.68168 · doi:10.1007/978-3-030-89247-0_12 |
| [12] | van Eerd J, Groote JF, Hijma P, Martens J, Osama M, Wijs A. Innermost many-sorted term rewriting on GPUs. Sci. Comput. Program., 2023. 225:102910. URL https://doi.org/10.1016/j.scico.2022. 102910. · doi:10.1016/j.scico.2022.102910 |
| [13] | Baudon T, Fuhs C, Gonnord L. Analysing Parallel Complexity of Term Rewriting. In: Villanueva A (ed.), Logic-Based Program Synthesis and Transformation -32nd International Symposium, LOPSTR 2022, Tbilisi, Georgia, September 21-23, 2022, Proceedings, volume 13474 of Lecture Notes in Computer Science. Springer, 2022 pp. 3-23. URL https://doi.org/10.1007/978-3-031-16767-6_1. · Zbl 1522.68253 · doi:10.1007/978-3-031-16767-6_1 |
| [14] | Noschinski L, Emmes F, Giesl J. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Autom. Reason., 2013. 51(1):27-56. URL https://doi.org/10.1007/ s10817-013-9277-6. · Zbl 1314.68174 · doi:10.1007/s10817-013-9277-6 |
| [15] | Lankford DS. Canonical algebraic simplification in computational logic. Technical Report ATP-25, University of Texas, 1975. |
| [16] | Fuhs C, Giesl J, Middeldorp A, Schneider-Kamp P, Thiemann R, Zankl H. SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva J, Sakallah KA (eds.), Theory and Applications of Satisfiability Testing -SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science. Springer, 2007 pp. 340-354. URL https://doi.org/10.1007/978-3-540-72788-0_33. · Zbl 1214.68352 · doi:10.1007/978-3-540-72788-0_33 |
| [17] | Borralleras C, Lucas S, Oliveras A, Rodríguez-Carbonell E, Rubio A. SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reason., 2012. 48(1):107-131. URL https://doi.org/10. 1007/s10817-010-9196-8. · Zbl 1243.68210 · doi:10.1007/s10817-010-9196-8 |
| [18] | Giesl J, Aschermann C, Brockschmidt M, Emmes F, Frohn F, Fuhs C, Hensel J, Otto C, Plücker M, Schneider-Kamp P, Ströder T, Swiderski S, Thiemann R. Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason., 2017. 58(1):3-31. Web interface and download: https:// aprove.informatik.rwth-aachen.de/, URL https://doi.org/10.1007/s10817-016-9388-y. · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [19] | Avanzini M, Moser G, Schaper M. TcT: Tyrolean Complexity Tool. In: Chechik M, Raskin J (eds.), Tools and Algorithms for the Construction and Analysis of Systems -22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science. Springer, 2016 pp. 407-423. Web interface and download: https://www.uibk.ac.at/en/ theoretical-computer-science/research/software/tct/, URL https://doi.org/10.1007/ 978-3-662-49674-9_24. · Zbl 1360.68008 · doi:10.1007/978-3-662-49674-9_24 |
| [20] | Kop C, Nishida N. Term Rewriting with Logical Constraints. In: Fontaine P, Ringeissen C, Schmidt RA (eds.), Frontiers of Combining Systems -9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science. Springer, 2013 pp. 343-358. URL https://doi.org/10.1007/978-3-642-40885-4_24. · Zbl 1398.68276 · doi:10.1007/978-3-642-40885-4_24 |
| [21] | Fuhs C, Kop C, Nishida N. Verifying Procedural Programs via Constrained Rewriting Induction. ACM Trans. Comput. Log., 2017. 18(2):14:1-14:50. URL https://doi.org/10.1145/3060143. · Zbl 1367.68248 · doi:10.1145/3060143 |
| [22] | Kop C. Higher Order Termination. Ph.D. thesis, VU Amsterdam, 2012. |
| [23] | Guo L, Kop C. Higher-Order LCTRSs and Their Termination. In: Weirich S (ed.), Programming Languages and Systems -33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14577 of Lecture Notes in Computer Science. Springer, 2024 pp. 331-357. URL https://doi.org/10.1007/978-3-031-57267-8_13. · doi:10.1007/978-3-031-57267-8_13 |
| [24] | Baader F, Nipkow T. Term rewriting and all that. Cambridge Univ. Press, 1998. ISBN 978-0-521-45520-6. |
| [25] | Hirokawa N, Moser G. Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando A, Baumgartner P, Dowek G (eds.), Automated Reasoning, 4th International Joint Conference, IJ-CAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science. Springer, 2008 pp. 364-379. URL https://doi.org/10.1007/978-3-540-71070-7_32. · Zbl 1165.68390 · doi:10.1007/978-3-540-71070-7_32 |
| [26] | Hirokawa N, Moser G. Automated Complexity Analysis Based on Context-Sensitive Rewriting. In: Dowek G (ed.), Rewriting and Typed Lambda Calculi -Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science. Springer, 2014 pp. 257-271. URL https://doi.org/10.1007/978-3-319-08918-8_18. · Zbl 1416.68092 · doi:10.1007/978-3-319-08918-8_18 |
| [27] | Avanzini M, Moser G. A combination framework for complexity. Information and Computation, 2016. 248:22-55. URL https://doi.org/10.1016/j.ic.2015.12.007. · Zbl 1339.68135 · doi:10.1016/j.ic.2015.12.007 |
| [28] | Naaf M, Frohn F, Brockschmidt M, Fuhs C, Giesl J. Complexity Analysis for Term Rewriting by Integer Transition Systems. In: Dixon C, Finger M (eds.), Frontiers of Combining Systems -11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings, volume 10483 of Lecture Notes in Computer Science. Springer, 2017 pp. 132-150. URL https://doi.org/10.1007/ 978-3-319-66167-4_8. · Zbl 1495.68116 · doi:10.1007/978-3-319-66167-4_8 |
| [29] | Frohn F, Giesl J, Hensel J, Aschermann C, Ströder T. Lower Bounds for Runtime Complexity of Term Rewriting. J. Autom. Reason., 2017. 59(1):121-163. URL https://doi.org/10.1007/ s10817-016-9397-x. · Zbl 1409.68254 · doi:10.1007/s10817-016-9397-x |
| [30] | Moser G, Schneckenreither M. Automated amortised resource analysis for term rewrite systems. Sci. Comput. Program., 2020. 185. URL https://doi.org/10.1016/j.scico.2019.102306. · doi:10.1016/j.scico.2019.102306 |
| [31] | Arts T, Giesl J. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science, 2000. 236:133-178. · Zbl 0938.68051 |
| [32] | Hong H, Jakus D. Testing Positiveness of Polynomials. J. Autom. Reason., 1998. 21(1):23-38. URL https://doi.org/10.1023/A:1005983105493. · Zbl 0916.68084 · doi:10.1023/A:1005983105493 |
| [33] | Blelloch GE, Greiner J. Parallelism in Sequential Functional Languages. In: Williams J (ed.), Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. ACM, 1995 pp. 226-237. URL https: //doi.org/10.1145/224164.224210. · doi:10.1145/224164.224210 |
| [34] | Thiemann R, Sternagel C, Giesl J, Schneider-Kamp P. Loops under Strategies ... Continued. In: Kirchner H, Muñoz CA (eds.), Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming, IWS 2010, Edinburgh, UK, 9th July 2010, volume 44 of EPTCS. 2010 pp. 51-65. URL https://doi.org/10.4204/EPTCS.44.4. · doi:10.4204/EPTCS.44.4 |
| [35] | van Oostrom V. Remarks on the full parallel innermost strategy, 2023. URL http://www.javakade.nl/ research/pdf/fpi.pdf. |
| [36] | Fuhs C, Giesl J, Middeldorp A, Schneider-Kamp P, Thiemann R, Zankl H. Maximal Termination. In: Voronkov A (ed.), Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science. Springer, 2008 pp. 110-125. URL https://doi.org/10.1007/978-3-540-70590-1_8. · Zbl 1145.68446 · doi:10.1007/978-3-540-70590-1_8 |
| [37] | Lamport L. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 1978. 21(7):558-565. URL https://doi.org/10.1145/359545.359563. · Zbl 0378.68027 · doi:10.1145/359545.359563 |
| [38] | Wiki. Termination Problems DataBase (TPDB). http://termination-portal.org/wiki/TPDB. |
| [39] | Giesl J, Rubio A, Sternagel C, Waldmann J, Yamada A. The Termination and Complexity Competition. In: Beyer D, Huisman M, Kordon F, Steffen B (eds.), Tools and Algorithms for the Construction and Analysis of Systems -25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science. Springer, 2019 pp. 156-166. URL https://doi.org/10.1007/978-3-030-17502-3_10. · doi:10.1007/978-3-030-17502-3_10 |
| [40] | Wiki. The International Termination Competition (TermComp). http://termination-portal.org/ wiki/Termination_Competition. |
| [41] | Lucas S. Context-sensitive Rewriting. ACM Comput. Surv., 2021. 53(4):78:1-78:36. URL https: //doi.org/10.1145/3397677. · doi:10.1145/3397677 |
| [42] | Flores-Montoya A, Hähnle R. Resource Analysis of Complex Programs with Cost Equations. In: Garrigue J (ed.), Programming Languages and Systems -12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, volume 8858 of Lecture Notes in Computer Science. Springer, 2014 pp. 275-295. URL https://doi.org/10.1007/978-3-319-12736-1_15. · Zbl 1453.68047 · doi:10.1007/978-3-319-12736-1_15 |
| [43] | Flores-Montoya A. Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds.), FM 2016: Formal Methods -21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science. 2016 pp. 254-273. URL https://doi.org/10.1007/978-3-319-48989-6_16. · doi:10.1007/978-3-319-48989-6_16 |
| [44] | Avanzini M, Felgenhauer B. Type introduction for runtime complexity analysis. In: WST ’14. 2014 pp. 1-5. Available from http://www.easychair.org/smart-program/VSL2014/WST-proceedings.pdf. |
| [45] | Knuth DE, Bendix PB. Simple Word Problems in Universal Algebras. In: Leech J (ed.), Computational Problems in Abstract Algebra. Pergamon Press, 1970 pp. 263-297. · Zbl 0188.04902 |
| [46] | Rosen BK. Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM, 1973. 20(1):160-187. URL https://doi.org/10.1145/321738.321750. · Zbl 0267.68013 · doi:10.1145/321738.321750 |
| [47] | Huet GP. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems. J. ACM, 1980. 27(4):797-821. URL https://doi.org/10.1145/322217.322230. · Zbl 0458.68007 · doi:10.1145/322217.322230 |
| [48] | Community. The International Confluence Competition (CoCo). http://project-coco.uibk.ac.at/. |
| [49] | Baudon T, Fuhs C, Gonnord L. On Confluence of Parallel-Innermost Term Rewriting. In: Winkler S, Rocha C (eds.), Proceedings of the 11th International Workshop on Confluence. 2022 pp. 31-36. URL http://cl-informatik.uibk.ac.at/iwc/2022/proceedings.pdf. |
| [50] | Gramlich B. Termination and confluence: properties of structured rewrite systems. Ph.D. thesis, Kaiser-slautern University of Technology, Germany, 1996. URL https://d-nb.info/949807389. |
| [51] | Stump A, Sutcliffe G, Tinelli C. StarExec: A Cross-Community Infrastructure for Logic Solving. In: Demri S, Kapur D, Weidenbach C (eds.), Automated Reasoning -7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, volume 8562 of Lecture Notes in Computer Science. Springer, 2014 pp. 367-373. https://www.starexec.org/, URL https://doi.org/10.1007/978-3-319-08587-6_28. · doi:10.1007/978-3-319-08587-6_28 |
| [52] | URL https://www.dcs.bbk.ac.uk/ carsten/eval/parallel_complexity_journal/. |
| [53] | TCT, version from the Termination and Complexity Competitions 2020 -2022. URL https://www. starexec.org/starexec/secure/details/solver.jsp?id=29575. |
| [54] | Hirokawa N, Nagele J, Middeldorp A. Cops and CoCoWeb: Infrastructure for Confluence Tools. In: Automated Reasoning -9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of LNCS. Springer, 2018 pp. 346-353. See also: https://cops.uibk.ac.at/, URL https://doi.org/10. 1007/978-3-319-94205-6_23. · doi:10.1007/978-3-319-94205-6_23 |
| [55] | Albert E, Arenas P, Genaim S, Zanardini D. Task-level analysis for a language with async/finish parallelism. In: Vitek J, Sutter BD (eds.), Proceedings of the ACM SIGPLAN/SIGBED 2011 conference on Languages, compilers, and tools for embedded systems, LCTES 2011, Chicago, IL, USA, April 11-14, 2011. ACM, 2011 pp. 21-30. URL https://doi.org/10.1145/1967677.1967681. · doi:10.1145/1967677.1967681 |
| [56] | Albert E, Arenas P, Genaim S, Puebla G, Zanardini D. Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci., 2012. 413(1):142-159. URL https://doi.org/10.1016/j.tcs.2011.07.009. · Zbl 1236.68042 · doi:10.1016/j.tcs.2011.07.009 |
| [57] | Hoffmann J, Aehlig K, Hofmann M. Resource Aware ML. In: Madhusudan P, Seshia SA (eds.), Computer Aided Verification -24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 |
| [58] | Proceedings, volume 7358 of Lecture Notes in Computer Science. Springer, 2012 pp. 781-786. URL https://doi.org/10.1007/978-3-642-31424-7_64. · doi:10.1007/978-3-642-31424-7_64 |
| [59] | Winkler S, Moser G. Runtime Complexity Analysis of Logically Constrained Rewriting. In: Fernández M (ed.), Logic-Based Program Synthesis and Transformation -30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings, volume 12561 of Lecture Notes in Computer Science. Springer, 2020 pp. 37-55. URL https://doi.org/10.1007/978-3-030-68446-4_2. · Zbl 07496640 · doi:10.1007/978-3-030-68446-4_2 |
| [60] | Hofbauer D, Lautemann C. Termination Proofs and the Length of Derivations. In: Dershowitz N (ed.), Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings, volume 355 of Lecture Notes in Computer Science. Springer, 1989 pp. 167-177. URL https://doi.org/10.1007/3-540-51081-8_107. · Zbl 1503.68116 · doi:10.1007/3-540-51081-8_107 |
| [61] | Shintani K, Hirokawa N. Compositional Confluence Criteria. In: Felty AP (ed.), 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2022 pp. 28:1-28:19. URL https://doi.org/10.4230/LIPIcs.FSCD.2022.28. · Zbl 1541.68184 · doi:10.4230/LIPIcs.FSCD.2022.28 |
| [62] | Shintani K, Hirokawa N. Compositional Confluence Criteria. Log. Methods Comput. Sci., 2024. 20(1). |
| [63] | Gutiérrez R, Vítores M, Lucas S. Confluence Framework: Proving Confluence with CONFident. In: Vil-lanueva A (ed.), Logic-Based Program Synthesis and Transformation -32nd International Symposium, LOP-STR 2022, Tbilisi, Georgia, September 21-23, 2022, Proceedings, volume 13474 of Lecture Notes in Com-puter Science. Springer, 2022 pp. 24-43. URL https://doi.org/10.1007/978-3-031-16767-6_2. · doi:10.1007/978-3-031-16767-6_2 |
| [64] | Contejean E, Courtieu P, Forest J, Pons O, Urbain X. Automated Certified Proofs with CiME3. In: Schmidt-Schauß M (ed.), Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 -June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2011 pp. 21-30. URL https://doi.org/10.4230/LIPIcs. RTA.2011.21. · Zbl 1236.68219 · doi:10.4230/LIPIcs.RTA.2011.21 |
| [65] | Blanqui F, Koprowski A. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci., 2011. 21(4):827-859. URL https://doi.org/10.1017/S0960129511000120. · Zbl 1223.68101 · doi:10.1017/S0960129511000120 |
| [66] | Thiemann R, Sternagel C. Certification of Termination Proofs Using CeTA. In: Berghofer S, Nipkow T, Ur-ban C, Wenzel M (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science. Springer, 2009 pp. 452-468. URL https://doi.org/10.1007/978-3-642-03359-9_31. · Zbl 1252.68265 · doi:10.1007/978-3-642-03359-9_31 |
| [67] | van der Weide N, Vale D, Kop C. Certifying Higher-Order Polynomial Interpretations. In: Naumowicz A, Thiemann R (eds.), 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2023 pp. 30:1-30:20. URL https://doi.org/10.4230/LIPIcs.ITP.2023.30. · doi:10.4230/LIPIcs.ITP.2023.30 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
