{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:47Z","timestamp":1750306787040,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T00:00:00Z","timestamp":1379289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001316","name":"University of Kent","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001316","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,9,16]]},"DOI":"10.1145\/2505879.2505886","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"37-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Proofs you can believe in"],"prefix":"10.1145","author":[{"given":"Jael","family":"Kriener","sequence":"first","affiliation":[{"name":"University of Kent, Canterbury, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[{"name":"University of Kent, Canterbury, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[{"name":"IRISA, University of Rennes I, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,9,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Abstract Interpretation of Declarative Languages. Ellis Horwood","author":"Abramsky","year":"1987","unstructured":"{ Abramsky and Hankin, 1987} Abramsky , S. and Hankin , C . ( 1987 ). Abstract Interpretation of Declarative Languages. Ellis Horwood . {Abramsky and Hankin, 1987} Abramsky, S. and Hankin, C. (1987). Abstract Interpretation of Declarative Languages. Ellis Horwood."},{"key":"e_1_3_2_1_2_1","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky","year":"1994","unstructured":"{ Abramsky and Jung, 1994} Abramsky , S. and Jung , A . ( 1994 ). Domain theory . In Abramsky, S., Gabbay, D., and Maibaum, T. S. E., editors, Handbook of Logic in Computer Science , pages 1 -- 168 . Oxford University Press . {Abramsky and Jung, 1994} Abramsky, S. and Jung, A. (1994). Domain theory. In Abramsky, S., Gabbay, D., and Maibaum, T. S. E., editors, Handbook of Logic in Computer Science, pages 1--168. Oxford University Press."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151650"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_10"},{"key":"e_1_3_2_1_5_1","volume-title":"22nd International Conference, TPHOLs 2009, Munich, Germany, August 17--20, 2009. Proceedings","volume":"5674","author":"Berghofer","year":"2009","unstructured":"{ Berghofer et al. , 2009 } Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M., editors (2009). 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. {Berghofer et al., 2009} Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M., editors (2009). 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."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389461"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.012"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90197-P"},{"key":"e_1_3_2_1_10_1","volume-title":"Lattice Theory","author":"Birkhoff","year":"1967","unstructured":"{ Birkhoff , 1967} Birkhoff, G. ( 1967 ). Lattice Theory . In Colloquium Publications, volume 25 . Amererican Mathematical Society , 3. edition. {Birkhoff, 1967} Birkhoff, G. (1967). Lattice Theory. In Colloquium Publications, volume 25. Amererican Mathematical Society, 3. edition."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000120"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"{\n      Cheney\n     and Urban 2004} \n      Cheney J.\n     and \n      Urban C\n  . (\n  2004\n  ). \n  αProlog: A Logic Programming Language with Names Binding and α-Equivalence\n  . In Demoen B. and Lifschitz V. editors ICLP volume \n  3132\n   of \n  Lecture Notes in Computer Science pages \n  269\n  --\n  283\n  . \n  Springer\n  .  {Cheney and Urban 2004} Cheney J. and Urban C. (2004). αProlog: A Logic Programming Language with Names Binding and α-Equivalence. In Demoen B. and Lifschitz V. editors ICLP volume 3132 of Lecture Notes in Computer Science pages 269--283. Springer.","DOI":"10.1007\/978-3-540-27775-0_19"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90055-8"},{"key":"e_1_3_2_1_18_1","volume-title":"The CompCert formally verified C compiler","author":"CompCert Development Team","year":"2012","unstructured":"{ CompCert Development Team , 2012} CompCert Development Team ( 2012 ). The CompCert formally verified C compiler . http:\/\/compcert.inria.fr\/. {CompCert Development Team, 2012} CompCert Development Team (2012). The CompCert formally verified C compiler. http:\/\/compcert.inria.fr\/."},{"key":"e_1_3_2_1_19_1","volume-title":"Version 8.3. INRIA","author":"Coq Development Team","year":"2010","unstructured":"{ Coq Development Team , 2010} Coq Development Team ( 2010 ). The Coq Proof Assistant Reference Manual , Version 8.3. INRIA . http:\/\/coq.inria.fr\/refman\/. {Coq Development Team, 2010} Coq Development Team (2010). The Coq Proof Assistant Reference Manual, Version 8.3. INRIA. http:\/\/coq.inria.fr\/refman\/."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/232706.232734"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90072-L"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(88)90007-6"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000032"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"{\n      Felty\n     et al. 1988\n  } Felty A. P. Gunter E. L. Hannan J. Miller D. Nadathur G. and Scedrov A. (1988). Lambda-Prolog: An Extended Logic Programming Language. In Lusk E. L. and Overbeek R. A. editors CADE volume \n  310\n   of \n  Lecture Notes in Computer Science pages \n  754\n  --\n  755\n  . \n  Springer\n  .   {Felty et al. 1988} Felty A. P. Gunter E. L. Hannan J. Miller D. Nadathur G. and Scedrov A. (1988). Lambda-Prolog: An Extended Logic Programming Language. In Lusk E. L. and Overbeek R. A. editors CADE volume 310 of Lecture Notes in Computer Science pages 754--755. Springer.","DOI":"10.1007\/BFb0012882"},{"key":"e_1_3_2_1_26_1","series-title":"LNCS","first-page":"1","volume-title":"ICALP","author":"Gabbrielli","year":"1991","unstructured":"{ Gabbrielli and Levi, 1991} Gabbrielli , M. and Levi , G . ( 1991 ). On the Semantics of Logic Programs . In ICALP , volume 510 of LNCS , pages 1 -- 19 . Springer . {Gabbrielli and Levi, 1991} Gabbrielli, M. and Levi, G. (1991). On the Semantics of Logic Programs. In ICALP, volume 510 of LNCS, pages 1--19. Springer."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"{\n      Gallagher 2003} Gallagher J. P.\n   (\n  2003\n  ). \n  A Program Transformation for Backwards Analysis of Logic Programs\n  . In Bruynooghe M. editor LOPSTR volume \n  3018\n   of \n  Lecture Notes in Computer Science pages \n  92\n  --\n  105\n  . \n  Springer\n  .  {Gallagher 2003} Gallagher J. P. (2003). A Program Transformation for Backwards Analysis of Logic Programs. In Bruynooghe M. editor LOPSTR volume 3018 of Lecture Notes in Computer Science pages 92--105. Springer.","DOI":"10.1007\/978-3-540-25938-1_8"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"issue":"2","key":"e_1_3_2_1_31_1","first-page":"95","article-title":"} Gonthier, G. and Mahboubi, A. (2010). An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","unstructured":"{ Gonthier and Mahboubi , 2010 } Gonthier, G. and Mahboubi, A. (2010). An introduction to small scale reflection in Coq . Journal of Formalised Reasoning , 3 ( 2 ): 95 -- 152 . {Gonthier and Mahboubi, 2010} Gonthier, G. and Mahboubi, A. (2010). An introduction to small scale reflection in Coq. Journal of Formalised Reasoning, 3(2):95--152.","journal-title":"Journal of Formalised Reasoning"},{"key":"e_1_3_2_1_32_1","first-page":"45","volume-title":"Abstract Interpretation of Declarative Languages","author":"Hudak","year":"1987","unstructured":"{ Hudak , 1987 } Hudak, P. (1987). A Semantic Model of Reference Counting and its Abstraction . In Abstract Interpretation of Declarative Languages , pages 45 -- 62 . Ellis Horwood. {Hudak, 1987} Hudak, P. (1987). A Semantic Model of Reference Counting and its Abstraction. In Abstract Interpretation of Declarative Languages, pages 45--62. Ellis Horwood."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90032-X"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068402001436"},{"key":"e_1_3_2_1_35_1","series-title":"LNCS","first-page":"315","volume-title":"ICLP","author":"King","year":"2003","unstructured":"{ King and Lu, 2003} King , A. and Lu , L . ( 2003 ). Forward versus Backward Verification of Logic Programs . In ICLP , volume 2916 of LNCS , pages 315 -- 330 . Springer . {King and Lu, 2003} King, A. and Lu, L. (2003). Forward versus Backward Verification of Logic Programs. In ICLP, volume 2916 of LNCS, pages 315--330. Springer."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.2307\/2267778"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000160"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_40_1","volume-title":"ICLP, page 945","author":"Levi","year":"1991","unstructured":"{ Levi , 1991} Levi, G. ( 1991 ). On the Semantics of Logic Programs . In ICLP, page 945 . MIT Press . {Levi, 1991} Levi, G. (1991). On the Semantics of Logic Programs. In ICLP, page 945. MIT Press."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90035-2"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_43_1","series-title":"LNCS","first-page":"347","volume-title":"TPHOLs","author":"Pusch","year":"1996","unstructured":"{ Pusch , 1996} Pusch, C. ( 1996 ). Verification of Compiler Correctness for the WAM . In TPHOLs , volume 1125 of LNCS , pages 347 -- 361 . Springer . {Pusch, 1996} Pusch, C. (1996). Verification of Compiler Correctness for the WAM. In TPHOLs, volume 1125 of LNCS, pages 347--361. Springer."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(91)90026-L"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069795"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_7"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/321978.321991"}],"event":{"name":"PPDP '13: 15th International Symposium on Principles and Practice of Declarative Programming","sponsor":["Universidad Complutense de Madrid","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Madrid Spain","acronym":"PPDP '13"},"container-title":["Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505886","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2505879.2505886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:16Z","timestamp":1750232056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505886"}},"subtitle":["proving equivalences between Prolog semantics in Coq"],"short-title":[],"issued":{"date-parts":[[2013,9,16]]},"references-count":47,"alternative-id":["10.1145\/2505879.2505886","10.1145\/2505879"],"URL":"https:\/\/doi.org\/10.1145\/2505879.2505886","relation":{},"subject":[],"published":{"date-parts":[[2013,9,16]]},"assertion":[{"value":"2013-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}