{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:47:22Z","timestamp":1767926842639,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,18]],"date-time":"2016-09-18T00:00:00Z","timestamp":1474156800000},"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":[[2016,9,18]]},"DOI":"10.1145\/2976022.2976030","type":"proceedings-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T12:40:09Z","timestamp":1472215209000},"page":"43-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Applications of applicative proof search"],"prefix":"10.1145","author":[{"given":"Liam","family":"O'Connor","sequence":"first","affiliation":[{"name":"UNSW, Australia \/ Data61, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,9,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Presburger arithmetic solver for agda. https:\/\/github.com\/ gallais\/agda-presburger","author":"Allais G.","year":"2015","unstructured":"G. Allais . Presburger arithmetic solver for agda. https:\/\/github.com\/ gallais\/agda-presburger , 2015 . G. Allais. Presburger arithmetic solver for agda. https:\/\/github.com\/ gallais\/agda-presburger, 2015."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1256049011"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0222-y"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30473-6_5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"doi: 10.1145\/5397.5399.    10.1145\/5397.5399\ndoi: 10.1145\/5397.5399.","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_3_2_1_8_1","volume-title":"Report on a conference sponsored by the NATO Science Committee","author":"Dijkstra E. W.","year":"1970","unstructured":"E. W. Dijkstra . Report on a conference sponsored by the NATO Science Committee , Rome . In Software Engineering Techniques , Apr. 1970 . E. W. Dijkstra. Report on a conference sponsored by the NATO Science Committee, Rome. In Software Engineering Techniques, Apr. 1970."},{"key":"e_1_3_2_1_9_1","first-page":"138","volume-title":"The Origin of Concurrent Programming","author":"Dijkstra E. W.","unstructured":"E. W. Dijkstra . Cooperating sequential processes. In P. Hansen, editor , The Origin of Concurrent Programming , pages 65\u2013 138 . Springer New York, 2002. ISBN 978-1-4419-2986-0. doi: 10.1007\/978-1-4757-3472-0_2. P. Dybjer, Q. Haiyan, and M. Takeyama. Combining testing and proving in dependent type theory. In Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics, TPHOLS \u201903, pages 188\u2013203, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. ISBN 978-3-540-45130-3. doi: 10.1007\/10930755_12. 10.1007\/978-1-4757-3472-0_2 E. W. Dijkstra. Cooperating sequential processes. In P. Hansen, editor, The Origin of Concurrent Programming, pages 65\u2013138. Springer New York, 2002. ISBN 978-1-4419-2986-0. doi: 10.1007\/978-1-4757-3472-0_2. P. Dybjer, Q. Haiyan, and M. Takeyama. Combining testing and proving in dependent type theory. In Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics, TPHOLS \u201903, pages 188\u2013203, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. ISBN 978-3-540-45130-3. doi: 10.1007\/10930755_12."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"doi: 10.1016\/j.infsof.2004.07.002.    10.1016\/j.infsof.2004.07.002\ndoi: 10.1016\/j.infsof.2004.07.002.","DOI":"10.1088\/1126-6708\/2004\/07\/002"},{"key":"e_1_3_2_1_11_1","series-title":"Mathematical Aspects of Computer Science","first-page":"31","volume-title":"Proceedings of a Symposium on Applied Mathematics","author":"Floyd R. W.","year":"1967","unstructured":"R. W. Floyd . Assigning Meanings to Programs . In J. T. Schwartz, editor, Proceedings of a Symposium on Applied Mathematics , volume 19 of Mathematical Aspects of Computer Science , pages 19\u2013 31 , Providence, 1967 . American Mathematical Society . R. W. Floyd. Assigning Meanings to Programs. In J. T. Schwartz, editor, Proceedings of a Symposium on Applied Mathematics, volume 19 of Mathematical Aspects of Computer Science, pages 19\u201331, Providence, 1967. American Mathematical Society."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_13_1","first-page":"1185","volume-title":"A proof of the kepler conjecture. Annals of mathematics","author":"Hales T. C.","year":"2005","unstructured":"T. C. Hales . A proof of the kepler conjecture. Annals of mathematics , pages 1065\u2013 1185 , 2005 . T. C. Hales. A proof of the kepler conjecture. Annals of mathematics, pages 1065\u20131185, 2005."},{"key":"e_1_3_2_1_14_1","volume-title":"T. Coquand, H. Lombardi, and M.-F","author":"Hales T. C.","year":"2006","unstructured":"T. C. Hales . Introduction to the flyspeck project . In T. Coquand, H. Lombardi, and M.-F . Roy, editors, Mathematics, Algorithms, Proofs , number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany , 2006 . T. C. Hales. Introduction to the flyspeck project. In T. Coquand, H. Lombardi, and M.-F. Roy, editors, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006."},{"key":"e_1_3_2_1_15_1","unstructured":"Internationales Begegnungsund Forschungszentrum f\u00fcr Informatik (IBFI) Schloss Dagstuhl Germany.  Internationales Begegnungsund Forschungszentrum f\u00fcr Informatik (IBFI) Schloss Dagstuhl Germany."},{"key":"e_1_3_2_1_16_1","volume-title":"Ring solver for agda. https:\/\/github.com\/wjzz\/ Agda-reflection-for-semiring-solver","author":"Jedynak W.","year":"2015","unstructured":"W. Jedynak . Ring solver for agda. https:\/\/github.com\/wjzz\/ Agda-reflection-for-semiring-solver , 2015 . W. Jedynak. Ring solver for agda. https:\/\/github.com\/wjzz\/ Agda-reflection-for-semiring-solver, 2015."},{"key":"e_1_3_2_1_17_1","volume-title":"Auto in Agda: programming proof search. Submitted to ICFP","author":"Kokke P.","year":"2014","unstructured":"P. Kokke and W. Swierstra . Auto in Agda: programming proof search. Submitted to ICFP 2014 , http:\/\/www.staff.science.uu. nl\/~swier004\/Publications\/AutoInAgda.pdf, 2014. P. Kokke and W. Swierstra. Auto in Agda: programming proof search. Submitted to ICFP 2014, http:\/\/www.staff.science.uu. nl\/~swier004\/Publications\/AutoInAgda.pdf, 2014."},{"key":"e_1_3_2_1_18_1","first-page":"94","volume-title":"Acta Philosophica Fennica","volume":"16","author":"Kripke S. A.","year":"1963","unstructured":"S. A. Kripke . Semantical considerations on modal logic . In Acta Philosophica Fennica , volume 16 , pages 83\u2013 94 , 1963 . S. A. Kripke. Semantical considerations on modal logic. In Acta Philosophica Fennica, volume 16, pages 83\u201394, 1963."},{"key":"e_1_3_2_1_19_1","volume-title":"LogiCal Project","year":"2004","unstructured":"The Coq development team. The Coq proof assistant reference manual . LogiCal Project , 2004 . The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004."},{"key":"e_1_3_2_1_20_1","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"Nipkow T.","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL: a proof assistant for higher-order logic , volume 2283 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: a proof assistant for higher-order logic, volume 2283."},{"key":"e_1_3_2_1_21_1","unstructured":"Springer Science & Business Media 2002.  Springer Science & Business Media 2002."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_1_23_1","volume-title":"Foundational Property-Based Testing. In ITP 2015 - 6th conference on Interactive Theorem Proving","volume":"9236","author":"Paraskevopoulou Z.","year":"2015","unstructured":"Z. Paraskevopoulou , C. Hritcu , M. D\u00e9n\u00e8s , L. Lampropoulos , and B. C. Pierce . Foundational Property-Based Testing. In ITP 2015 - 6th conference on Interactive Theorem Proving , volume 9236 of Lecture Notes in Computer Science, Nanjing, China , Aug. 2015 . Springer. Z. Paraskevopoulou, C. Hritcu, M. D\u00e9n\u00e8s, L. Lampropoulos, and B. C. Pierce. Foundational Property-Based Testing. In ITP 2015 - 6th conference on Interactive Theorem Proving, volume 9236 of Lecture Notes in Computer Science, Nanjing, China, Aug. 2015. Springer."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"doi: 10.1007\/978-3-319-22102-1\\_22.    10.1007\/978-3-319-22102-1\ndoi: 10.1007\/978-3-319-22102-1\\_22.","DOI":"10.1007\/978-3-319-22102-1"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_13"},{"key":"e_1_3_2_1_29_1","first-page":"4503","volume":"978","author":"ACM","unstructured":"ACM . ISBN 978-1 - 4503 - 2326 -0. doi: 10.1145\/2500365.2500579. 10.1145\/2500365.2500579 ACM. ISBN 978-1-4503-2326-0. doi: 10.1145\/2500365.2500579.","journal-title":"ISBN"}],"event":{"name":"ICFP'16: ACM SIGPLAN International Conference on Functional Programming","location":"Nara Japan","acronym":"ICFP'16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 1st International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2976022.2976030","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2976022.2976030","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:56:16Z","timestamp":1750222576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2976022.2976030"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,18]]},"references-count":29,"alternative-id":["10.1145\/2976022.2976030","10.1145\/2976022"],"URL":"https:\/\/doi.org\/10.1145\/2976022.2976030","relation":{},"subject":[],"published":{"date-parts":[[2016,9,18]]},"assertion":[{"value":"2016-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}