{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:29:42Z","timestamp":1755998982352},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"Association for Computing Machinery and Morgan & Claypool","isbn-type":[{"value":"9781970001273","type":"print"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,2]]},"DOI":"10.1145\/2841316","type":"monograph","created":{"date-parts":[[2016,2,5]],"date-time":"2016-02-05T15:51:48Z","timestamp":1454687508000},"update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Verified Functional Programming in Agda"],"prefix":"10.1145","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[{"name":"The University of Iowa"}]}],"member":"320","published-online":{"date-parts":[[2016,2]]},"reference":[{"key":"e_1_4_1_1_1","series-title":"Electronic Proceedings in Theoretical Computer Science","first-page":"28","volume-title":"Proc. Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR","author":"Abel A.","year":"2010","unstructured":"A. Abel . Miniagda: Integrating sized and dependent types . In A. Bove, E. Komendantskaya, and M. Niqui, editors, Proc. Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR 2010 , Edinburgh , UK , July 15, 2010, vol. 43 of Electronic Proceedings in Theoretical Computer Science . pp. 14\u2014 28 , 2010. Available at http:\/\/eptcs.web.cse.unsw.edu.au\/content.cgi?PAR2010. A. Abel. Miniagda: Integrating sized and dependent types. In A. Bove, E. Komendantskaya, and M. Niqui, editors, Proc. Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR 2010, Edinburgh, UK, July 15, 2010, vol. 43 of Electronic Proceedings in Theoretical Computer Science. pp. 14\u201428, 2010. Available at http:\/\/eptcs.web.cse.unsw.edu.au\/content.cgi?PAR2010."},{"key":"e_1_4_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_5"},{"key":"e_1_4_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500591"},{"key":"e_1_4_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_4_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/10704973_6"},{"key":"e_1_4_1_6_1","volume-title":"Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science . Springer , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, 2004."},{"key":"e_1_4_1_7_1","series-title":"LNCS","first-page":"121","volume-title":"Automated Reasoning (IJCAR","author":"B\u00f6hme S.","year":"2010","unstructured":"S. B\u00f6hme and T. Nipkow . Sledgehammer: Judgement day . In J. Giesl and R. H\u00e4hnle, editors, Automated Reasoning (IJCAR 2010 ), vol. 6173 of LNCS , Springer . pp. 107\u2014 121 , 2010. DOI: 10.1007\/978-3-642-14203-1_9. 10.1007\/978-3-642-14203-1_9 S. B\u00f6hme and T. Nipkow. Sledgehammer: Judgement day. In J. Giesl and R. H\u00e4hnle, editors, Automated Reasoning (IJCAR 2010), vol. 6173 of LNCS, Springer. pp. 107\u2014121, 2010. DOI: 10.1007\/978-3-642-14203-1_9."},{"key":"e_1_4_1_8_1","first-page":"5","article-title":"History of lambda-calculus and combinatory logic","author":"Cardone F.","year":"2006","unstructured":"F. Cardone and J. R. Hindley . History of lambda-calculus and combinatory logic . Handbook of the History of Logic , 5 , 2006 . F. Cardone and J. R. Hindley. History of lambda-calculus and combinatory logic. Handbook of the History of Logic, 5, 2006.","journal-title":"Handbook of the History of Logic"},{"key":"e_1_4_1_9_1","volume-title":"Certified Programming with Dependent Types","author":"Chlipala A.","year":"2011","unstructured":"A. Chlipala . Certified Programming with Dependent Types . MIT Press , 2011 . A. Chlipala. Certified Programming with Dependent Types. MIT Press, 2011."},{"key":"e_1_4_1_10_1","volume-title":"The Calculi of Lambda Conversion","author":"Church A.","year":"1941","unstructured":"A. Church . The Calculi of Lambda Conversion . Princeton University Press , 1941 . Annals of Mathematics Studies, no. 6. A. Church. The Calculi of Lambda Conversion. Princeton University Press, 1941. Annals of Mathematics Studies, no. 6."},{"key":"e_1_4_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_6"},{"key":"e_1_4_1_12_1","doi-asserted-by":"crossref","unstructured":"E.\n      Contejean\n     and \n      P.\n      Corbineau\n  . \n  Reflecting proofs in first-order logic with equality\n  . In R. Nieuwenhuis editor 20th International Conference on Automated Deduction (CADE) vol. \n  3632\n   of \n  Lecture Notes in Computer Science Springer\n  . pp. 7\u2014\n  22\n  . 2005. DOI: 10.1007\/11532231_2.    10.1007\/11532231_2\nE. Contejean and P. Corbineau. Reflecting proofs in first-order logic with equality. In R. Nieuwenhuis editor 20th International Conference on Automated Deduction (CADE) vol. 3632 of Lecture Notes in Computer Science Springer. pp. 7\u201422. 2005. DOI: 10.1007\/11532231_2.","DOI":"10.1007\/11532231_2"},{"key":"e_1_4_1_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019964114625"},{"key":"e_1_4_1_14_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.185.5"},{"key":"e_1_4_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003104"},{"key":"e_1_4_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034796"},{"key":"e_1_4_1_17_1","first-page":"82","volume-title":"Structured Programming","author":"Dijkstra E. W.","year":"1972","unstructured":"E. W. Dijkstra . Notes on Structured Programming . In O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, editors, Structured Programming , Academic Press , 1972 , pp. 1\u2014 82 . E. W. Dijkstra. Notes on Structured Programming. In O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare, editors, Structured Programming, Academic Press, 1972, pp. 1\u201482."},{"key":"e_1_4_1_18_1","unstructured":"A. Diller. Bracket abstraction algorithms. http:\/\/www.cantab.net\/users\/antoni.diller\/brackets\/intro.html 2014.  A. Diller. Bracket abstraction algorithms. http:\/\/www.cantab.net\/users\/antoni.diller\/brackets\/intro.html 2014."},{"key":"e_1_4_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45699-6_4"},{"key":"e_1_4_1_20_1","volume-title":"Functional Swift. objc.io","author":"Eidhof C.","year":"2014","unstructured":"C. Eidhof , F. Kugler , and W. Swierstra . Functional Swift. objc.io , 2014 . Available at http:\/\/www.objc.io\/books\/functional-swift\/. C. Eidhof, F. Kugler, and W. Swierstra. Functional Swift. objc.io, 2014. Available at http:\/\/www.objc.io\/books\/functional-swift\/."},{"key":"e_1_4_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508701"},{"key":"e_1_4_1_22_1","unstructured":"M. Giovannini. Braun trees 2010. Blog post at http:\/\/alaska-kamtchatka.blogspot.com\/2010\/02\/braun-trees.html.  M. Giovannini. Braun trees 2010. Blog post at http:\/\/alaska-kamtchatka.blogspot.com\/2010\/02\/braun-trees.html."},{"key":"e_1_4_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_4_1_25_1","volume-title":"Parsing Techniques - A Practical Guide","author":"Grune D.","unstructured":"D. Grune and C.J.H. Jacobs . Parsing Techniques - A Practical Guide ( 2 nd ed.), Springer . D. Grune and C.J.H. Jacobs. Parsing Techniques - A Practical Guide (2nd ed.), Springer.","edition":"2"},{"key":"e_1_4_1_26_1","unstructured":"R. Hindley. The root-2 proof as an example of non-constructivity. Available from the author's Web page http:\/\/www.users.waitrose.com\/~hindley\/ 2014.  R. Hindley. The root-2 proof as an example of non-constructivity. Available from the author's Web page http:\/\/www.users.waitrose.com\/~hindley\/ 2014."},{"key":"e_1_4_1_27_1","unstructured":"P. Hudak J. Peterson and J. Fasel. A gentle introduction to Haskell Version 98. http:\/\/www.haskell.org\/tutorial\/monads.html 2000.  P. Hudak J. Peterson and J. Fasel. A gentle introduction to Haskell Version 98. http:\/\/www.haskell.org\/tutorial\/monads.html 2000."},{"key":"e_1_4_1_28_1","first-page":"68","volume-title":"Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical Reports.","author":"Hurd J.","year":"2003","unstructured":"J. Hurd . First-order proof tactics in higher-order logic theorem provers. In Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical Reports. pp. 56\u2014 68 , 2003 . J. Hurd. First-order proof tactics in higher-order logic theorem provers. In Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical Reports. pp. 56\u201468, 2003."},{"key":"e_1_4_1_30_1","unstructured":"D. Ilik. Normalization of g\u00f6del's system t extended with control delimited at the type of natural numbers. http:\/\/www.lix.polytechnique.fr\/~danko\/PPDP-2014-tutorial\/. PPDP 2014 Distilled Tutorial.  D. Ilik. Normalization of g\u00f6del's system t extended with control delimited at the type of natural numbers. http:\/\/www.lix.polytechnique.fr\/~danko\/PPDP-2014-tutorial\/. PPDP 2014 Distilled Tutorial."},{"key":"e_1_4_1_31_1","volume-title":"Accessed","author":"Kiselyov O.","year":"2015","unstructured":"O. Kiselyov . Type-safe functional formatted IO. http:\/\/okmij.org\/ftp\/typed-formatting\/FPrintScan.html . Accessed July , 2015 . O. Kiselyov. Type-safe functional formatted IO. http:\/\/okmij.org\/ftp\/typed-formatting\/FPrintScan.html. Accessed July, 2015."},{"key":"e_1_4_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1844-9"},{"key":"e_1_4_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863551"},{"key":"e_1_4_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_4_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628163"},{"key":"e_1_4_1_36_1","article-title":"new spam-killer hints at the future of coding","author":"Metz C.","year":"2015","unstructured":"C. Metz . Facebook's new spam-killer hints at the future of coding . Wired Magazine , September 2015 . Available online at http:\/\/www.wired.com\/2015\/09\/facebooks-new-anti-spam-system-hints-future-coding\/. C. Metz. Facebook's new spam-killer hints at the future of coding. Wired Magazine, September 2015. Available online at http:\/\/www.wired.com\/2015\/09\/facebooks-new-anti-spam-system-hints-future-coding\/.","journal-title":"Wired Magazine"},{"key":"e_1_4_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512671"},{"key":"e_1_4_1_38_1","volume-title":"Programming in Martin-L\u00f6f Type Theory: An Introduction","author":"Nordstr\u00f6m B.","year":"1990","unstructured":"B. Nordstr\u00f6m , K. Petersson , and J. M. Smith . Programming in Martin-L\u00f6f Type Theory: An Introduction . Clarendon , 1990 . B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f Type Theory: An Introduction. Clarendon, 1990."},{"key":"e_1_4_1_40_1","volume-title":"Personal Communication","author":"Norell U.","year":"2015","unstructured":"U. Norell . Personal Communication , 2015 . U. Norell. Personal Communication, 2015."},{"key":"e_1_4_1_41_1","series-title":"Lecture Notes in Computer Science","first-page":"266","volume-title":"Advanced Functional Programming, 6th International School, AFP","author":"Norell U.","year":"2008","unstructured":"U. Norell and J. Chapman . Dependently typed programming in Agda . In P.W.M. Koopman, R. Plasmeijer, and S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008 , Heijen, The Netherlands , May 2008, Revised Lectures, vol. 5832 of Lecture Notes in Computer Science , Springer . pp. 230\u2014 266 , 2009. U. Norell and J. Chapman. Dependently typed programming in Agda. In P.W.M. Koopman, R. Plasmeijer, and S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, vol. 5832 of Lecture Notes in Computer Science, Springer. pp. 230\u2014266, 2009."},{"key":"e_1_4_1_42_1","volume-title":"Software Foundations. Electronic textbook","author":"Pierce B. C.","year":"2015","unstructured":"B. C. Pierce , C. Casinghino , M. Gaboardi , M. Greenberg , C. Hri\u0163cu , V. Sjoberg , and B. Yorgey . Software Foundations. Electronic textbook , 2015 . http:\/\/www.cis.upenn.edu\/~bcpierce\/sf. B. C. Pierce, C. Casinghino, M. Gaboardi, M. Greenberg, C. Hri\u0163cu, V. Sjoberg, and B. Yorgey. Software Foundations. Electronic textbook, 2015. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf."},{"key":"e_1_4_1_43_1","first-page":"179","volume-title":"Set Theory, Arithmetic, and Foundations of Mathematics","author":"Troelstra A. S.","year":"2011","unstructured":"A. S. Troelstra . History of constructivism in the 20th century . In J. Kennedy and R. Kossak, editors, Set Theory, Arithmetic, and Foundations of Mathematics , Cambridge University Press . pp. 150\u2014 179 , 2011 . A. S. Troelstra. History of constructivism in the 20th century. In J. Kennedy and R. Kossak, editors, Set Theory, Arithmetic, and Foundations of Mathematics, Cambridge University Press. pp. 150\u2014179, 2011."},{"key":"e_1_4_1_44_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-642-39091-3","volume-title":"Implementation and Application of Functional Languages - 24th International Symposium, IFL, Revised Selected Papers","author":"van der Walt P.","year":"2013","unstructured":"P. van der Walt and W. Swierstra . Engineering proof by reflection in Agda . In R. Hinze, editor, Implementation and Application of Functional Languages - 24th International Symposium, IFL, Revised Selected Papers , vol. 8241 of Lecture Notes in Computer Science , Springer . pp. 157\u2014 173 , 2013 . DOI: 10.1007\/978-3-642-41582-1_10. 10.1007\/978-3-642-41582-1_10 P. van der Walt and W. Swierstra. Engineering proof by reflection in Agda. In R. Hinze, editor, Implementation and Application of Functional Languages - 24th International Symposium, IFL, Revised Selected Papers, vol. 8241 of Lecture Notes in Computer Science, Springer. pp. 157\u2014173, 2013. DOI: 10.1007\/978-3-642-41582-1_10."}],"container-title":[],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2841316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,5]],"date-time":"2023-01-05T10:36:18Z","timestamp":1672914978000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/book\/10.1145\/2841316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2]]},"ISBN":["9781970001273"],"references-count":41,"alternative-id":["10.1145\/2841316"],"URL":"https:\/\/doi.org\/10.1145\/2841316","relation":{},"subject":[],"published":{"date-parts":[[2016,2]]},"assertion":[{"value":"2016-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}