{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:03:10Z","timestamp":1771059790639,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T00:00:00Z","timestamp":1599004800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004063","name":"Knut och Alice Wallenbergs Stiftelse","doi-asserted-by":"publisher","award":["WASP"],"award-info":[{"award-number":["WASP"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["2016-06204"],"award-info":[{"award-number":["2016-06204"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["2014-04849"],"award-info":[{"award-number":["2014-04849"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,2]]},"DOI":"10.1145\/3462172.3462192","type":"proceedings-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T22:06:52Z","timestamp":1627078012000},"page":"67-78","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing"],"prefix":"10.1145","author":[{"given":"S\u00f3lr\u00fan Halla","family":"Einarsd\u00f3ttir","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"given":"Nicholas","family":"Smallbone","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"given":"Moa","family":"Johansson","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122961"},{"key":"e_1_3_2_1_2_1","first-page":"9","article-title":"Theory exploration with Theorema. Analele Universitatii Din Timisoara, ser","volume":"38","author":"Buchberger Bruno","year":"2000","unstructured":"Bruno Buchberger . 2000 . Theory exploration with Theorema. Analele Universitatii Din Timisoara, ser . Matematica-Informatica 38 , 2(2000), 9 \u2013 32 . Bruno Buchberger. 2000. Theory exploration with Theorema. Analele Universitatii Din Timisoara, ser. Matematica-Informatica 38, 2(2000), 9\u201332.","journal-title":"Matematica-Informatica"},{"key":"e_1_3_2_1_3_1","volume-title":"Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic 4 (12","author":"Buchberger Bruno","year":"2006","unstructured":"Bruno Buchberger , Adrian Craciun , Tudor Jebelean , Laura Kov\u00e1cs , Temur Kutsia , Koji Nakagawa , Florina Piroi , Nikolaj Popov , Judit Robu , Markus Rosenkranz , and Wolfgang Windsteiger . 2006 . Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic 4 (12 2006), 470\u2013504. https:\/\/doi.org\/10.1016\/j.jal.2005.10.006 10.1016\/j.jal.2005.10.006 Bruno Buchberger, Adrian Craciun, Tudor Jebelean, Laura Kov\u00e1cs, Temur Kutsia, Koji Nakagawa, Florina Piroi, Nikolaj Popov, Judit Robu, Markus Rosenkranz, and Wolfgang Windsteiger. 2006. Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic 4 (12 2006), 470\u2013504. https:\/\/doi.org\/10.1016\/j.jal.2005.10.006"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_5_1","first-page":"279","article-title":"IsaPlanner: A Prototype Proof Planner in Isabelle","volume":"2741","author":"Dixon Lucas","year":"2003","unstructured":"Lucas Dixon and Jacques D.\u00a0 Fleuriot . 2003 . IsaPlanner: A Prototype Proof Planner in Isabelle . LNCS (LNAI) 2741 , 279 \u2013 283 . https:\/\/doi.org\/10.1007\/978-3-540-45085-6_22 10.1007\/978-3-540-45085-6_22 Lucas Dixon and Jacques D.\u00a0Fleuriot. 2003. IsaPlanner: A Prototype Proof Planner in Isabelle. LNCS (LNAI) 2741, 279\u2013283. https:\/\/doi.org\/10.1007\/978-3-540-45085-6_22","journal-title":"LNCS (LNAI)"},{"key":"e_1_3_2_1_6_1","unstructured":"Lucas Dixon and Moa Johansson. 2007. IsaPlanner 2: A Proof Planner for Isabelle.  Lucas Dixon and Moa Johansson. 2007. IsaPlanner 2: A Proof Planner for Isabelle."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_27"},{"key":"e_1_3_2_1_8_1","volume-title":"Language Hierarchies and Interfaces, Friedrich\u00a0L. Bauer, E.\u00a0W. Dijkstra, A.\u00a0Ershov, M.\u00a0Griffiths, C.\u00a0A.\u00a0R. Hoare, W.\u00a0A","author":"Hoare R.","unstructured":"C.\u00a0A.\u00a0 R. Hoare . 1976. Proof of correctness of data representations . In Language Hierarchies and Interfaces, Friedrich\u00a0L. Bauer, E.\u00a0W. Dijkstra, A.\u00a0Ershov, M.\u00a0Griffiths, C.\u00a0A.\u00a0R. Hoare, W.\u00a0A . Wulf, and Klaus Samelson (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 183\u2013193. C.\u00a0A.\u00a0R. Hoare. 1976. Proof of correctness of data representations. In Language Hierarchies and Interfaces, Friedrich\u00a0L. Bauer, E.\u00a0W. Dijkstra, A.\u00a0Ershov, M.\u00a0Griffiths, C.\u00a0A.\u00a0R. Hoare, W.\u00a0A. Wulf, and Klaus Samelson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 183\u2013193."},{"key":"e_1_3_2_1_9_1","volume-title":"Advanced Functional Programming, J.\u00a0Jeuring and E.\u00a0Meijer (Eds.)","author":"Hughes John","unstructured":"John Hughes . 1995. The Design of a Pretty-printing Library . In Advanced Functional Programming, J.\u00a0Jeuring and E.\u00a0Meijer (Eds.) . Springer Verlag , LNCS 925, 53\u201396. John Hughes. 1995. The Design of a Pretty-printing Library. In Advanced Functional Programming, J.\u00a0Jeuring and E.\u00a0Meijer (Eds.). Springer Verlag, LNCS 925, 53\u201396."},{"key":"e_1_3_2_1_10_1","volume-title":"Trends in Functional Programming, William\u00a0J","author":"Hughes John","unstructured":"John Hughes . 2020. How to Specify It . In Trends in Functional Programming, William\u00a0J . Bowman and Ronald Garcia (Eds.). Springer International Publishing , Cham , 58\u201383. John Hughes. 2020. How to Specify It. In Trends in Functional Programming, William\u00a0J. Bowman and Ronald Garcia (Eds.). Springer International Publishing, Cham, 58\u201383."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00244460"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9193-y"},{"key":"e_1_3_2_1_14_1","volume-title":"MATHsAiD: Automated mathematical theory exploration. Applied Intelligence (23","author":"McCasland L.","year":"2017","unstructured":"R.\u00a0 L. McCasland , A. Bundy , and P.\u00a0 F. Smith . 2017. MATHsAiD: Automated mathematical theory exploration. Applied Intelligence (23 Jun 2017 ). https:\/\/doi.org\/10.1007\/s10489-017-0954-8 10.1007\/s10489-017-0954-8 R.\u00a0L. McCasland, A. Bundy, and P.\u00a0F. Smith. 2017. MATHsAiD: Automated mathematical theory exploration. Applied Intelligence (23 Jun 2017). https:\/\/doi.org\/10.1007\/s10489-017-0954-8"},{"key":"e_1_3_2_1_15_1","volume-title":"Scheme-based theorem discovery and concept invention. Expert systems with applications 39, 2","author":"Montano-Rivas Omar","year":"2012","unstructured":"Omar Montano-Rivas , Roy McCasland , Lucas Dixon , and Alan Bundy . 2012. Scheme-based theorem discovery and concept invention. Expert systems with applications 39, 2 ( 2012 ), 1637\u20131646. Omar Montano-Rivas, Roy McCasland, Lucas Dixon, and Alan Bundy. 2012. Scheme-based theorem discovery and concept invention. Expert systems with applications 39, 2 (2012), 1637\u20131646."},{"key":"e_1_3_2_1_16_1","unstructured":"Markus\u00a0N. Rabe Dennis Lee Kshitij Bansal and Christian Szegedy. 2020. Mathematical Reasoning via Self-supervised Skip-tree Training. arxiv:2006.04757\u00a0[cs.LG]  Markus\u00a0N. Rabe Dennis Lee Kshitij Bansal and Christian Szegedy. 2020. Mathematical Reasoning via Self-supervised Skip-tree Training. arxiv:2006.04757\u00a0[cs.LG]"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_3_2_1_18_1","volume-title":"Quick specifications for the busy programmer. Journal of Functional Programming 27","author":"Smallbone Nicholas","year":"2017","unstructured":"Nicholas Smallbone , Moa Johansson , Koen Claessen , and Maximilian Algehed . 2017. Quick specifications for the busy programmer. Journal of Functional Programming 27 ( 2017 ). https:\/\/doi.org\/10.1017\/S0956796817000090 10.1017\/S0956796817000090 Nicholas Smallbone, Moa Johansson, Koen Claessen, and Maximilian Algehed. 2017. Quick specifications for the busy programmer. Journal of Functional Programming 27 (2017). https:\/\/doi.org\/10.1017\/S0956796817000090"},{"key":"e_1_3_2_1_19_1","unstructured":"Don Stewart. 2007. Roll Your Own Window Manager: Part 1: Defining and Testing a Model. https:\/\/donsbot.wordpress.com\/2007\/05\/01\/roll-your-own-window-manager-part-1-defining-and-testing-a-model\/  Don Stewart. 2007. Roll Your Own Window Manager: Part 1: Defining and Testing a Model. https:\/\/donsbot.wordpress.com\/2007\/05\/01\/roll-your-own-window-manager-part-1-defining-and-testing-a-model\/"},{"key":"e_1_3_2_1_20_1","volume-title":"Xmonad. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop","author":"Stewart Don","year":"2007","unstructured":"Don Stewart and Spencer Sjanssen . 2007 . Xmonad. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop ( Freiburg, Germany) (Haskell \u201907). Association for Computing Machinery, New York, NY, USA, 119. https:\/\/doi.org\/10.1145\/1291201.1291218 10.1145\/1291201.1291218 Don Stewart and Spencer Sjanssen. 2007. Xmonad. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop (Freiburg, Germany) (Haskell \u201907). Association for Computing Machinery, New York, NY, USA, 119. https:\/\/doi.org\/10.1145\/1291201.1291218"}],"event":{"name":"IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages","location":"Canterbury United Kingdom","acronym":"IFL 2020"},"container-title":["Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462192","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462172.3462192","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:34Z","timestamp":1750191454000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,2]]},"references-count":20,"alternative-id":["10.1145\/3462172.3462192","10.1145\/3462172"],"URL":"https:\/\/doi.org\/10.1145\/3462172.3462192","relation":{},"subject":[],"published":{"date-parts":[[2020,9,2]]},"assertion":[{"value":"2021-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}