{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:53:30Z","timestamp":1750308810030,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,18]],"date-time":"2010-01-18T00:00:00Z","timestamp":1263772800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,1,18]]},"DOI":"10.1145\/1706356.1706370","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T20:15:04Z","timestamp":1263932104000},"page":"63-72","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["A3PAT, an approach for certified automated termination proofs"],"prefix":"10.1145","author":[{"given":"\u00c9velyne","family":"Contejean","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Sud 11 and CNRS, Orsay F-91405, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Sud 11 and CNRS, Orsay F-91405, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Sud 11 and CNRS and \u00c9cole nationale sup\u00e9rieure d'informatique pour l'industrie et l'entreprise, Orsay F-91405, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[{"name":"Conservatoire National des Arts et M\u00e9tiers, Paris F-75141, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Pons","sequence":"additional","affiliation":[{"name":"Conservatoire National des Arts et M\u00e9tiers, Paris F-75141, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Forest","sequence":"additional","affiliation":[{"name":"\u00c9cole nationale sup\u00e9rieure d'informatique pour l'industrie et l'entreprise, \u00c9vry F-91025, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_28"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_18"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","volume-title":"Theory and Practice of Software Development","author":"Arts T.","year":"1997","unstructured":"T. Arts and J. Giesl . Automatically Proving Termination Where Simplification Orderings Fail . In M. Bidoit and M. Dauchet, editors, Theory and Practice of Software Development , volume 1214 of LNCS , Lille, France, Apr . 1997 . Springer-Verlag . T. Arts and J. Giesl. Automatically Proving Termination Where Simplification Orderings Fail. In M. Bidoit and M. Dauchet, editors, Theory and Practice of Software Development, volume 1214 of LNCS, Lille, France, Apr. 1997. Springer-Verlag."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021939521172"},{"key":"e_1_3_2_1_7_1","unstructured":"F. Blanqui S. Coupet-Grimal W. Delobel S. Hinderer and A. Koprowski. Color a Coq library on rewriting and termination. In {24}.  F. Blanqui S. Coupet-Grimal W. Delobel S. Hinderer and A. Koprowski. Color a Coq library on rewriting and termination. In {24}."},{"key":"e_1_3_2_1_8_1","unstructured":"\u00c9. Contejean. The Coccinelle library for rewriting. URL http:\/\/www.lri.fr\/ contejea\/Coccinelle\/coccinelle.html.  \u00c9. Contejean. The Coccinelle library for rewriting. URL http:\/\/www.lri.fr\/ contejea\/Coccinelle\/coccinelle.html."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"\u00c9. Contejean.\n  A certified AC matching algorithm\n  . In V. van Oostrom editor RTA'04 volume \n  3091\n   of\n  LNCS pages \n  70\n  --\n  84 Aachen Germany June \n  2004\n  . \n  Springer-Verlag\n  .  \u00c9. Contejean. A certified AC matching algorithm. In V. van Oostrom editor RTA'04 volume 3091 ofLNCS pages 70--84 Aachen Germany June 2004. Springer-Verlag.","DOI":"10.1007\/978-3-540-25979-4_5"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"E. Contejean and C. March\u00e9. CiME: Completion Modulo E. In {23} pages 416--419. URL http:\/\/cime.lri.fr\/.   E. Contejean and C. March\u00e9. CiME: Completion Modulo E. In {23} pages 416--419. URL http:\/\/cime.lri.fr\/.","DOI":"10.1007\/3-540-61464-8_70"},{"key":"e_1_3_2_1_11_1","first-page":"71","volume-title":"WST'03","author":"March\u00e9 C.","year":"2003","unstructured":"\u00c9. Contejean, C. March\u00e9 , B. Monate , and X. Urbain . Proving termination of rewriting with CiME. In A. Rubio, editor , WST'03 , pages 71 -- 73 , June 2003 . URL http:\/\/cime.lri.fr. Technical Report DSIC II\/15\/03, Univ. Polit\u00e9cnica de Valencia, Spain. \u00c9. Contejean, C. March\u00e9, B. Monate, and X. Urbain. Proving termination of rewriting with CiME. In A. Rubio, editor, WST'03, pages 71--73, June 2003. URL http:\/\/cime.lri.fr. Technical Report DSIC II\/15\/03, Univ. Polit\u00e9cnica de Valencia, Spain."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9022-x"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_10"},{"key":"e_1_3_2_1_14_1","series-title":"LNCS","volume-title":"Proceedings of Colog'88","author":"Coquand T.","year":"1988","unstructured":"T. Coquand and C. Paulin-Mohring . Inductively defined types . In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of Colog'88 , volume 417 of LNCS , Tallinn, USSR , 1988 . Springer-Verlag . T. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of Colog'88, volume 417 of LNCS, Tallinn, USSR, 1988. Springer-Verlag."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_17"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11266-9_24"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"e_1_3_2_1_18_1","volume-title":"Handbook of Theoretical Computer Science","author":"Dershowitz N.","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud . Rewrite systems . In J. van Leeuwen, editor, Handbook of Theoretical Computer Science , volume B, pages 243-- 320 . North-Holland , 1990 . N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243--320. North-Holland, 1990."},{"key":"e_1_3_2_1_19_1","unstructured":"D. Doligez. Zenon. URL http:\/\/focal.inria.fr\/zenon\/.  D. Doligez. Zenon. URL http:\/\/focal.inria.fr\/zenon\/."},{"key":"e_1_3_2_1_20_1","unstructured":"J. Endrullis. Jambox. URL http:\/\/joerg.endrullis.de\/index.html.  J. Endrullis. Jambox. URL http:\/\/joerg.endrullis.de\/index.html."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"e_1_3_2_1_22_1","series-title":"LNCS","first-page":"340","volume-title":"SAT'07","author":"Fuhs C.","year":"2007","unstructured":"C. Fuhs , A. Middeldorp , P. Schneider-Kamp , and H. Zankl . SAT solving for termination analysis with polynomial interpretations . In SAT'07 , volume 4501 of LNCS , pages 340 -- 354 , Lisbon, Portugal, May 2007 . Springer-Verlag . C. Fuhs, A. Middeldorp, P. Schneider-Kamp, and H. Zankl. SAT solving for termination analysis with polynomial interpretations. In SAT'07, volume 4501 of LNCS, pages340--354, Lisbon, Portugal, May 2007. Springer-Verlag."},{"key":"e_1_3_2_1_23_1","series-title":"LNCS","volume-title":"RTA'96","author":"Ganzinger H.","year":"1996","unstructured":"H. Ganzinger , editor. RTA'96 , volume 1103 of LNCS , New Brunswick, USA , July 1996 . Springer-Verlag . H. Ganzinger, editor. RTA'96, volume 1103 of LNCS, New Brunswick, USA, July 1996. Springer-Verlag."},{"key":"e_1_3_2_1_24_1","volume-title":"WST'06","author":"Geser A.","year":"2006","unstructured":"A. Geser and H. Sondergaard , editors . WST'06 , Aug. 2006 . A. Geser and H. Sondergaard, editors. WST'06, Aug. 2006."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0541"},{"key":"e_1_3_2_1_26_1","series-title":"LNAI","first-page":"165","volume-title":"LPAR'03","author":"Giesl J.","year":"2003","unstructured":"J. Giesl , R. Thiemann , P. Schneider-Kamp , and S. Falke . Improving Dependency Pairs . In LPAR'03 , volume 2850 of LNAI , pages 165 -- 179 , Almaty, Kazakhstan, Sep. 2003 . Springer-Verlag . J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke. Improving Dependency Pairs. In LPAR'03, volume 2850 of LNAI, pages165--179, Almaty, Kazakhstan, Sep. 2003. Springer-Verlag."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_3_2_1_28_1","first-page":"93","volume-title":"On proving termination by innermost termination. In {23}","author":"Gramlich B.","unstructured":"B. Gramlich . On proving termination by innermost termination. In {23} , pages 93 -- 107 . B. Gramlich. On proving termination by innermost termination. In {23}, pages 93--107."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.010"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_19"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"K.\n      Kusakari M.\n      Nakamura and \n      Y.\n      Toyama\n  . \n  Argument filtering transformation\n  . In G. Nadathur editor PPDP'99 volume \n  1702\n   of \n  LNCS pages \n  47\n  --\n  61 Paris France 1999\n  . \n  Springer-Verlag\n  .   K. Kusakari M. Nakamura and Y. Toyama. Argument filtering transformation. In G. Nadathur editor PPDP'99 volume 1702 of LNCS pages 47--61 Paris France 1999. Springer-Verlag.","DOI":"10.1007\/10704567_3"},{"key":"e_1_3_2_1_34_1","volume-title":"The termination competition","author":"March\u00e9 C.","year":"2006","unstructured":"C. March\u00e9 and H. Zantema . The termination competition 2006 . In {24}. URL http:\/\/www.lri.fr\/ marche\/termination-competition\/. C. March\u00e9 and H. Zantema. The termination competition 2006. In {24}. URL http:\/\/www.lri.fr\/ marche\/termination-competition\/."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021975117537"},{"key":"e_1_3_2_1_36_1","series-title":"LNCS","volume-title":"Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L.C. Paulson , and M. Wenzel . Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic . volume 2283 of LNCS , 2002 . Springer-Verlag . T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic. volume 2283 of LNCS, 2002. Springer-Verlag."},{"key":"e_1_3_2_1_37_1","volume-title":"June","author":"Development Team The Coq","year":"2008","unstructured":"The Coq Development Team . The Coq Proof Assistant Documentation -- Version V8.2 , June 2008 . URL http:\/\/coq.inria.fr\/refman\/. The Coq Development Team. The Coq Proof Assistant Documentation -- Version V8.2, June 2008. URL http:\/\/coq.inria.fr\/refman\/."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"e_1_3_2_1_39_1","series-title":"LNAI","first-page":"75","volume-title":"IJCAR'04","author":"Thiemann R.","year":"2004","unstructured":"R. Thiemann , J. Giesl , and P. Schneider-Kamp . Improved modular termination proofs using dependency pairs . In IJCAR'04 , volume 3097 of LNAI , pages 75 -- 90 , Cork, Ireland , 2004 . Springer-Verlag . R. Thiemann, J. Giesl, and P. Schneider-Kamp. Improved modular termination proofs using dependency pairs. In IJCAR'04, volume 3097 of LNAI, pages 75--90, Cork, Ireland, 2004. Springer-Verlag."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03177743"}],"event":{"name":"PEPM '10: Partial Evaluation and Program Manipulation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Madrid Spain","acronym":"PEPM '10"},"container-title":["Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706356.1706370","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1706356.1706370","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:19Z","timestamp":1750278379000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706356.1706370"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,18]]},"references-count":39,"alternative-id":["10.1145\/1706356.1706370","10.1145\/1706356"],"URL":"https:\/\/doi.org\/10.1145\/1706356.1706370","relation":{},"subject":[],"published":{"date-parts":[[2010,1,18]]},"assertion":[{"value":"2010-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}