{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:35Z","timestamp":1772164115342,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,11,5]],"date-time":"2018-11-05T00:00:00Z","timestamp":1541376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100012774","name":"Innovationsfonden","doi-asserted-by":"publisher","award":["7039-00072B"],"award-info":[{"award-number":["7039-00072B"]}],"id":[{"id":"10.13039\/100012774","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008394","name":"Det Frie Forskningsr\u00e5d","doi-asserted-by":"publisher","award":["0602-02327B"],"award-info":[{"award-number":["0602-02327B"]}],"id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,11,5]]},"DOI":"10.1145\/3278122.3278125","type":"proceedings-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:28:39Z","timestamp":1540380519000},"page":"147-160","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verification of high-level transformations with inductive refinement types"],"prefix":"10.1145","author":[{"given":"Ahmad Salim","family":"Al-Sibahi","sequence":"first","affiliation":[{"name":"University of Copenhagen, Denmark \/ Skanned, Denmark \/ IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas P.","family":"Jensen","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandar S.","family":"Dimovski","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark \/ Mother Teresa University, Macedonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,11,5]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"427","article-title":"Implementing Regular Tree Expressions","volume":"1991","author":"Aiken Alexander","year":"1991","unstructured":"Alexander Aiken and Brian R. Murphy . 1991 . Implementing Regular Tree Expressions . In FPLCA 1991. 427 - 447 . Alexander Aiken and Brian R. Murphy. 1991. Implementing Regular Tree Expressions. In FPLCA 1991. 427-447.","journal-title":"FPLCA"},{"key":"e_1_3_2_1_2_1","volume-title":"The Formal Semantics of Rascal Light. CoRR abs\/1703.02312","author":"Al-Sibahi Ahmad Salim","year":"2017","unstructured":"Ahmad Salim Al-Sibahi . 2017. The Formal Semantics of Rascal Light. CoRR abs\/1703.02312 ( 2017 ). http:\/\/arxiv.org\/abs\/1703.02312. Ahmad Salim Al-Sibahi. 2017. The Formal Semantics of Rascal Light. CoRR abs\/1703.02312 (2017). http:\/\/arxiv.org\/abs\/1703.02312."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2997364.2997382"},{"key":"e_1_3_2_1_4_1","volume-title":"Verification of High-Level Transformations with Inductive Refinement Types. ArXiv e-prints (Sept","author":"Al-Sibahi Ahmad Salim","year":"2018","unstructured":"Ahmad Salim Al-Sibahi , Thomas P. Jensen , Aleksandar S. Dimovski , and Andrzej Wasowski . 2018. Verification of High-Level Transformations with Inductive Refinement Types. ArXiv e-prints (Sept . 2018 ). arXiv:cs.PL\/1809.06336 https:\/\/arxiv.org\/abs\/1809.06336. Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski, and Andrzej Wasowski. 2018. Verification of High-Level Transformations with Inductive Refinement Types. ArXiv e-prints (Sept. 2018). arXiv:cs.PL\/1809.06336 https:\/\/arxiv.org\/abs\/1809.06336."},{"key":"e_1_3_2_1_5_1","first-page":"634","article-title":"Spatial Interpolants","volume":"2015","author":"Albarghouthi Aws","year":"2015","unstructured":"Aws Albarghouthi , Josh Berdine , Byron Cook , and Zachary Kincaid . 2015 . Spatial Interpolants . In ESOP 2015. 634 - 660 . Aws Albarghouthi, Josh Berdine, Byron Cook, and Zachary Kincaid. 2015. Spatial Interpolants. In ESOP 2015. 634-660.","journal-title":"ESOP"},{"key":"e_1_3_2_1_6_1","first-page":"116","article-title":"Dependency Analysis of Functional Specifications with Algebraic Data Structures","volume":"2015","author":"Andreescu Oana Fabiana","year":"2015","unstructured":"Oana Fabiana Andreescu , Thomas Jensen , and St\u00e9phane Lescuyer . 2015 . Dependency Analysis of Functional Specifications with Algebraic Data Structures . In ICFEM 2015. 116 - 133 . Oana Fabiana Andreescu, Thomas Jensen, and St\u00e9phane Lescuyer. 2015. Dependency Analysis of Functional Specifications with Algebraic Data Structures. In ICFEM 2015. 116-133.","journal-title":"ICFEM"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.11.003"},{"key":"e_1_3_2_1_8_1","volume-title":"Universes for Generic Programs and Proofs in Dependent Type Theory. 10, 4","author":"Benke Marcin","year":"2003","unstructured":"Marcin Benke , Peter Dybjer , and Patrik Jansson . 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. 10, 4 ( 2003 ), 265-289. Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. 10, 4 (2003), 265-289."},{"key":"e_1_3_2_1_9_1","first-page":"101","article-title":"Static and dynamic semantics of NoSQL languages","volume":"2013","author":"Benzaken V\u00e9ronique","year":"2013","unstructured":"V\u00e9ronique Benzaken , Giuseppe Castagna , Kim Nguyen , and J\u00e9r\u00f4me Sim\u00e9on . 2013 . Static and dynamic semantics of NoSQL languages . In POPL 2013. 101 - 114 . V\u00e9ronique Benzaken, Giuseppe Castagna, Kim Nguyen, and J\u00e9r\u00f4me Sim\u00e9on. 2013. Static and dynamic semantics of NoSQL languages. In POPL 2013. 101-114.","journal-title":"POPL"},{"key":"e_1_3_2_1_10_1","first-page":"29","article-title":"Certified Abstract Interpretation with Pretty-Big-Step Semantics","volume":"2015","author":"Bodin Martin","year":"2015","unstructured":"Martin Bodin , Thomas Jensen , and Alan Schmitt . 2015 . Certified Abstract Interpretation with Pretty-Big-Step Semantics . In CPP 2015. 29 - 40 . Martin Bodin, Thomas Jensen, and Alan Schmitt. 2015. Certified Abstract Interpretation with Pretty-Big-Step Semantics. In CPP 2015. 29-40.","journal-title":"CPP"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_1"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.11.003"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411210"},{"key":"e_1_3_2_1_14_1","first-page":"247","article-title":"Relational Inductive Shape Analysis","volume":"2008","author":"Evan Chang Bor-Yuh","year":"2008","unstructured":"Bor-Yuh Evan Chang and Xavier Rival . 2008 . Relational Inductive Shape Analysis . In POPL 2008. 247 - 260 . Bor-Yuh Evan Chang and Xavier Rival. 2008. Relational Inductive Shape Analysis. In POPL 2008. 247-260.","journal-title":"POPL"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.04.002"},{"key":"e_1_3_2_1_17_1","volume-title":"Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 243-268.","author":"Cousot Patrick","unstructured":"Patrick Cousot . 2003. Verification by Abstract Interpretation . In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 243-268. Patrick Cousot. 2003. Verification by Abstract Interpretation. In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 243-268."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224199"},{"key":"e_1_3_2_1_19_1","first-page":"159","article-title":"Modular Static Program Analysis","volume":"2002","author":"Cousot Patrick","year":"2002","unstructured":"Patrick Cousot and Radhia Cousot . 2002 . Modular Static Program Analysis . In CC 2002. 159 - 178 . Patrick Cousot and Radhia Cousot. 2002. Modular Static Program Analysis. In CC 2002. 159-178.","journal-title":"CC"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2635137"},{"key":"e_1_3_2_1_21_1","volume-title":"ICFP","author":"Darais David","year":"2017","unstructured":"David Darais , Nicholas Labich , Phuc C. Nguyen , and David Van Horn . 2017. Abstracting definitional interpreters (functional pearl). PACMPL 1 , ICFP ( 2017 ), 12:1-12:25. David Darais, Nicholas Labich, Phuc C. Nguyen, and David Van Horn. 2017. Abstracting definitional interpreters (functional pearl). PACMPL 1, ICFP (2017), 12:1-12:25."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.05.017"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"key":"e_1_3_2_1_24_1","first-page":"268","article-title":"Refinement Types for ML","volume":"1991","author":"Freeman Timothy S.","year":"1991","unstructured":"Timothy S. Freeman and Frank Pfenning . 1991 . Refinement Types for ML . In PLDI 1991. 268 - 277 . Timothy S. Freeman and Frank Pfenning. 1991. Refinement Types for ML. In PLDI 1991. 268-277.","journal-title":"PLDI"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375623"},{"key":"e_1_3_2_1_26_1","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison John","unstructured":"John Harrison . 2009. Handbook of Practical Logic and Automated Reasoning . Cambridge University Press . John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_3_2_1_28_1","volume-title":"Partial evaluation and automatic program generation","author":"Jones Neil D.","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . 1993. Partial evaluation and automatic program generation . Prentice Hall . Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Prentice Hall."},{"key":"e_1_3_2_1_29_1","volume-title":"EASY Metaprogramming with Rascal","author":"Klint Paul","unstructured":"Paul Klint , Tijs van der Storm , and Jurgen Vinju . 2011. EASY Metaprogramming with Rascal . In GTTSE III, Jo\u00e3o M. Fernandes, Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.). 222-289. Paul Klint, Tijs van der Storm, and Jurgen Vinju. 2011. EASY Metaprogramming with Rascal. In GTTSE III, Jo\u00e3o M. Fernandes, Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.). 222-289."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the Third International Workshop on Verification and Program Transformation, VPT@ETAPS 2015","author":"Alexei","year":"2015","unstructured":"Alexei P. Lisitsa and Andrei P. Nemytykh. 2015. Finite Countermodel Based Verification for Program Transformation (A Case Study) . In Proceedings of the Third International Workshop on Verification and Program Transformation, VPT@ETAPS 2015 , London, United Kingdom, 11th April 2015 . (EPTCS), Alexei Lisitsa, Andrei P. Nemytykh, and Alberto Pettorossi (Eds.), Vol. 199. 15-32. Alexei P. Lisitsa and Andrei P. Nemytykh. 2015. Finite Countermodel Based Verification for Program Transformation (A Case Study). In Proceedings of the Third International Workshop on Verification and Program Transformation, VPT@ETAPS 2015, London, United Kingdom, 11th April 2015. (EPTCS), Alexei Lisitsa, Andrei P. Nemytykh, and Alberto Pettorossi (Eds.), Vol. 199. 15-32."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2016.01.005"},{"key":"e_1_3_2_1_32_1","volume-title":"Haskell","author":"Mitchell Neil","year":"2007","unstructured":"Neil Mitchell and Colin Runciman . 2007. Uniform boilerplate and list processing . In Haskell 2007 , Freiburg , Germany . 49-60. Neil Mitchell and Colin Runciman. 2007. Uniform boilerplate and list processing. In Haskell 2007, Freiburg, Germany. 49-60."},{"key":"e_1_3_2_1_33_1","volume-title":"Jones","author":"Mycroft Alan","year":"1985","unstructured":"Alan Mycroft and Neil D . Jones . 1985 . A relational framework for abstract interpretation. In Programs as Data Objects . 156-171. Alan Mycroft and Neil D. Jones. 1985. A relational framework for abstract interpretation. In Programs as Data Objects. 156-171."},{"key":"e_1_3_2_1_34_1","first-page":"279","article-title":"An Analysis of Permutations in Arrays","volume":"2010","author":"Perrelle Valentin","year":"2010","unstructured":"Valentin Perrelle and Nicolas Halbwachs . 2010 . An Analysis of Permutations in Arrays . In VMCAI 2010. 279 - 294 . Valentin Perrelle and Nicolas Halbwachs. 2010. An Analysis of Permutations in Arrays. In VMCAI 2010. 279-294.","journal-title":"VMCAI"},{"key":"e_1_3_2_1_35_1","first-page":"129","article-title":"An Improved Unrolling-Based Decision Procedure for Algebraic Data Types","volume":"2013","author":"Pham Tuan-Hung","year":"2013","unstructured":"Tuan-Hung Pham and Michael W. Whalen . 2013 . An Improved Unrolling-Based Decision Procedure for Algebraic Data Types . In VSTTE 2013. 129 - 148 . Tuan-Hung Pham and Michael W. Whalen. 2013. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. In VSTTE 2013. 129-148.","journal-title":"VSTTE"},{"key":"e_1_3_2_1_36_1","first-page":"80","article-title":"Induction for SMT Solvers","volume":"2015","author":"Reynolds Andrew","year":"2015","unstructured":"Andrew Reynolds and Viktor Kuncak . 2015 . Induction for SMT Solvers . In VMCAI 2015. 80 - 98 . Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In VMCAI 2015. 80-98.","journal-title":"VMCAI"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_3_2_1_38_1","first-page":"489","article-title":"Construction of Abstract Domains for Heterogeneous Properties","volume":"2014","author":"Rival Xavier","year":"2014","unstructured":"Xavier Rival , Antoine Toubhans , and Bor-Yuh Evan Chang . 2014 . Construction of Abstract Domains for Heterogeneous Properties . In ISoLA 2014. 489 - 492 . Xavier Rival, Antoine Toubhans, and Bor-Yuh Evan Chang. 2014. Construction of Abstract Domains for Heterogeneous Properties. In ISoLA 2014. 489-492.","journal-title":"ISoLA"},{"key":"e_1_3_2_1_39_1","unstructured":"Mads Rosendahl. 2013. Abstract Interpretation as a Programming Language. In Semantics Abstract Interpretation and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday. 84-104.  Mads Rosendahl. 2013. Abstract Interpretation as a Programming Language. In Semantics Abstract Interpretation and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday . 84-104."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007734417713"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_3_2_1_43_1","volume-title":"Programming language concepts","author":"Sestoft Peter","unstructured":"Peter Sestoft and Niels Hallenberg . 2017. Programming language concepts . Springer . Peter Sestoft and Niels Hallenberg. 2017. Programming language concepts. Springer."},{"key":"e_1_3_2_1_44_1","series-title":"Lecture Notes in Computer Science","volume-title":"Lightweight Language Processing in Kiama","author":"Sloane Anthony M.","unstructured":"Anthony M. Sloane . 2011. Lightweight Language Processing in Kiama . In GTTSE III, Jo\u00e3oM. Fernandes, Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.). Lecture Notes in Computer Science , Vol. 6491 . Springer Berlin Heidelberg , 408-425. Anthony M. Sloane. 2011. Lightweight Language Processing in Kiama. In GTTSE III, Jo\u00e3oM. Fernandes, Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.). Lecture Notes in Computer Science, Vol. 6491. Springer Berlin Heidelberg, 408-425."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800002008"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_1_48_1","first-page":"375","article-title":"Reduced Product Combination of Abstract Domains for Shapes","volume":"2013","author":"Toubhans Antoine","year":"2013","unstructured":"Antoine Toubhans , Bor-Yuh Evan Chang , and Xavier Rival . 2013 . Reduced Product Combination of Abstract Domains for Shapes . In VMCAI 2013. 375 - 395 . Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival. 2013. Reduced Product Combination of Abstract Domains for Shapes. In VMCAI 2013. 375-395.","journal-title":"VMCAI"},{"key":"e_1_3_2_1_49_1","first-page":"209","article-title":"Abstract Refinement Types","volume":"2013","author":"Vazou Niki","year":"2013","unstructured":"Niki Vazou , Patrick Maxim Rondon , and Ranjit Jhala . 2013 . Abstract Refinement Types . In ESOP 2013. 209 - 228 . Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In ESOP 2013. 209-228.","journal-title":"ESOP"},{"key":"e_1_3_2_1_50_1","volume-title":"Information Systems","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1993. Information Systems . MIT Press , Chapter 12. Glynn Winskel. 1993. Information Systems. MIT Press, Chapter 12."},{"key":"e_1_3_2_1_51_1","unstructured":"Niklaus Wirth. 1996. Compiler Construction. Addison-Wesley.   Niklaus Wirth. 1996. Compiler Construction . Addison-Wesley."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"event":{"name":"GPCE '18: 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences","location":"Boston MA USA","acronym":"GPCE '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3278122.3278125","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3278122.3278125","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:54:09Z","timestamp":1750190049000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3278122.3278125"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,5]]},"references-count":52,"alternative-id":["10.1145\/3278122.3278125","10.1145\/3278122"],"URL":"https:\/\/doi.org\/10.1145\/3278122.3278125","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3393934.3278125","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,11,5]]},"assertion":[{"value":"2018-11-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}