{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T09:04:29Z","timestamp":1750323869590,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000690","name":"Research Councils UK","doi-asserted-by":"publisher","award":["EP\/T026952\/1, EP\/TO26960\/1, EP\/TO27037\/1"],"award-info":[{"award-number":["EP\/T026952\/1, EP\/TO26960\/1, EP\/TO27037\/1"]}],"id":[{"id":"10.13039\/501100000690","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575674","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"102-120","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively"],"prefix":"10.1145","author":[{"given":"Matthew L.","family":"Daggitt","sequence":"first","affiliation":[{"name":"Heriot-Watt University, UK"}]},{"given":"Robert","family":"Atkey","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"Wen","family":"Kokke","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, UK"}]},{"given":"Luca","family":"Arnaboldi","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"John Backes Pauline Bolignano Byron Cook Catherine Dodge Andrew Gacek Kasper Luckow Neha Rungta Oksana Tkachuk and Carsten Varming. 2018. Semantic-based automated reasoning for AWS access policies using SMT. In 2018 Formal Methods in Computer Aided Design (FMCAD). 1\u20139.","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00022-0"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796899003366"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03793-1_3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_3_2_1_10_1","unstructured":"Matthew L. Daggitt Wen Kokke Atkey Bob Natalia \u015alusarz and Marco Casadio. 2022. Vehicle. https:\/\/github.com\/vehicle-lang\/vehicle Accessed on 22.09.2022"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"volume-title":"Studies in Logic and the Foundations of Mathematics. 63","author":"Girard Jean-Yves","key":"e_1_3_2_1_13_1","unstructured":"Jean-Yves Girard. 1971. Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse, et son application \u00e0 l\u2019\u00e9limination de coupures dans l\u2019analyse et la th\u00e9orie des types. In Studies in Logic and the Foundations of Mathematics. 63, Elsevier, 63\u201392."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Hyondeuk Kim and Fabio Somenzi. 2006. Finite instantiations for integer difference logic. In 2006 Formal Methods in Computer Aided Design. 31\u201338.","DOI":"10.1109\/FMCAD.2006.13"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/MILCOM.2003.1290218"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. 1993. Functional unification of higher-order patterns. In [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. 64\u201374.","DOI":"10.1109\/LICS.1993.287599"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Ulf Norell. 2008. Dependently typed programming in Agda. In International school on advanced functional programming. 230\u2013266.","DOI":"10.1007\/978-3-642-04652-0_5"},{"volume-title":"Types and programming languages","author":"Pierce Benjamin C","key":"e_1_3_2_1_22_1","unstructured":"Benjamin C Pierce. 2002. Types and programming languages. MIT press."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:23)2022"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556946"},{"volume-title":"Program synthesis by sketching","author":"Solar-Lezama Armando","key":"e_1_3_2_1_25_1","unstructured":"Armando Solar-Lezama. 2008. Program synthesis by sketching. University of California, Berkeley."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_27_1","volume-title":"Liquid Haskell: Haskell as a theorem prover","author":"Vazou Niki","year":"2016","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a theorem prover. University of California, San Diego."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_1_29_1","volume-title":"Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31 (2018)."}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575674","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575674","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575674"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":29,"alternative-id":["10.1145\/3573105.3575674","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575674","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}