{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:41Z","timestamp":1694623961790},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,5]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            The close association between higher order functions (HOFs) and algorithmic skeletons is a promising source of automatic parallelisation of programs. A theorem proving approach to discovering HOFs in functional programs is presented. Our starting point is proof planning, an automated theorem proving technique in which high-level proof plans are used to guide proof search. We use proof planning to identify provably correct transformation rules that introduce HOFs. The approach has been implemented in the\n            <jats:italic>\u03bb Clam<\/jats:italic>\n            proof planner and tested on a range of examples. The work was conducted within the context of a parallelising compiler for Standard ML.\n          <\/jats:p>","DOI":"10.1007\/s00165-004-0054-5","type":"journal-article","created":{"date-parts":[[2005,3,21]],"date-time":"2005-03-21T14:38:34Z","timestamp":1111415914000},"page":"38-57","source":"Crossref","is-referenced-by-count":3,"title":["Discovering applications of higher order functions through proof planning"],"prefix":"10.1145","volume":"17","author":[{"given":"A.","family":"Cook","sequence":"first","affiliation":[{"name":"School of Mathematical and Computer Sciences, Heriot-Watt University, EH14 4AS, Riccarton, Edinburgh, Scotland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Ireland","sequence":"additional","affiliation":[{"name":"School of Mathematical and Computer Sciences, Heriot-Watt University, EH14 4AS, Riccarton, Edinburgh, Scotland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Michaelson","sequence":"additional","affiliation":[{"name":"School of Mathematical and Computer Sciences, Heriot-Watt University, EH14 4AS, Riccarton, Edinburgh, Scotland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Scaife","sequence":"additional","affiliation":[{"name":"VERIMAG, Centre Equation 2, Ave de Vignat, 38610, Griers, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"2","key":"p_1","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1080\/01495730108935268","article-title":"Towards parallel programming by transformation: the FAN skeleton framework","volume":"16","author":"Aldinucci M","year":"2001","journal-title":"Parallel Algorithms Appl."},{"key":"p_2","series-title":"Advances in Computation: theory and practice","volume-title":"Gorlatch S., Lengauer C, (eds) Constructive methods for parallel programming","author":"Ald M","year":"2002"},{"key":"p_3","first-page":"2","volume-title":"Lake Tahoe","author":"Alessandro Armando","year":"1997"},{"issue":"8","key":"p_4","first-page":"287","article-title":"Can Programming be Liberated from the Von Neumann Style","volume":"21","author":"Bac","year":"1978","journal-title":"Commun. ACM"},{"key":"p_5","volume-title":"Algebra of Programming","author":"Bd R","year":"1997"},{"key":"p_6","unstructured":"[BR] Brisset P Ridoux O. Prolog\/Mali. ftp.irisa.fr:\/local\/pm\/"},{"key":"p_7","volume-title":"In: Fox L, (ed) Advances in Programming and Non-numerical Computation.","author":"Barron DW","year":"1996"},{"key":"p_8","first-page":"221","article-title":"Turning eureka steps into calculations in automatic program synthesis. In: Clarke. SLH., (ed)","volume":"90","author":"Bundy A","year":"1990","journal-title":"Proceedings of UK IT"},{"key":"p_9","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","article-title":"Rippling: a heuristic for guiding inductive proofs","volume":"62","author":"Sv A","year":"1993","journal-title":"Artificial Intelligence"},{"key":"p_10","first-page":"111","volume-title":"Springer Berlin Heidelberg New York","author":"Bun A","year":"1998"},{"key":"p_11","volume-title":"Department of Artificial Intelligence","author":"Bv A","year":"1990"},{"key":"p_12","article-title":"Experiments with proof plans for induction","author":"Bv A","year":"1991","journal-title":"Appeared in Journal of Automated Reasoning"},{"issue":"1","key":"p_13","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00244462","article-title":"A calculus for and termination of rippling","volume":"16","author":"David Basin","year":"1996","journal-title":"J. Automated Reasoning"},{"key":"p_14","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable RL","year":"1986"},{"key":"p_15","volume-title":"The calculi of lambda conversion","author":"Chu A","year":"1941"},{"key":"p_16","volume-title":"London","author":"Col MI","year":"1989"},{"key":"p_17","first-page":"279","volume-title":"Proceedings of CADE'03","author":"Dixon L","year":"2003"},{"key":"p_18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF - A mechanised logic of computation","author":"Gordon MJ","year":"1979"},{"key":"p_19","volume-title":"Technical report memorandum: MIP-R-101, School of Artificial Intelligence","author":"Gor MJC","year":"1973"},{"issue":"2","key":"p_21","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1142\/S0129626400000238","article-title":"HDC: a higher-order language for divide conquer","volume":"10","author":"Herrmann CA","year":"2000","journal-title":"Parallel Processing Letters"},{"key":"p_22","first-page":"199","volume-title":"Taha W, (ed) Semantics, applications, and implementation of program generation, number 2196 in LNCS","author":"Herrmann CA","year":"2001"},{"key":"p_23","volume-title":"Department of Artificial Intelligence","author":"Hor C","year":"1988"},{"key":"p_24","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/10722298_11","volume-title":"Proceedings of 11th International Workshop on Implementation of Functional Languages (IFL'99)","author":"Hammond K","year":"2000"},{"issue":"1","key":"p_26","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00244460","article-title":"Productive use of failure in inductive proof","volume":"16","author":"Ireland A","year":"1996","journal-title":"J. Automated Reasoning"},{"key":"p_27","series-title":"Lecture Notes in Artificial Intelligence No. 624","first-page":"178","volume-title":"Voronkov A (ed) International conference on logic programming and automated reasoning - LPAR 92, St. Petersburg","author":"Ire A","year":"1992"},{"key":"p_28","first-page":"1","volume-title":"Lau KK, Clement T, (eds) Logic program synthesis and transformation","author":"Kraan I","year":"1993"},{"issue":"1","key":"p_29","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF00244461","article-title":"Middle-out reasoning for synthesis and induction","volume":"16","author":"Kraan I","year":"1996","journal-title":"J. Automated Reasoning"},{"key":"p_30","volume-title":"London","author":"Kel P","year":"1989"},{"key":"p_31","volume-title":"Introduction to metamathematics. North-Holand","author":"Kle SC","year":"1952"},{"key":"p_32","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","article-title":"Recursive functions of symbolic expressions and their computation by machine: Part 1","volume":"3","author":"Mc J","year":"1960","journal-title":"Communications of the ACM"},{"key":"p_33","first-page":"539","volume-title":"Clack C, Davie T, Hammond K (eds) Proceedings of 9th International Workshop on Implementation of Functional Languages, School of Mathematical and Computer Sciences","author":"Michaelson G","year":"1997"},{"key":"p_34","volume-title":"Rabhi F, Gorlatch S, (eds) Patterns and skeletons for parallel and distributed computing","author":"Michaelson G","year":"2000"},{"key":"p_35","first-page":"181","volume-title":"Nested Algorithmic skeletons from higher order functions. Parallel algorithms and applications: special issue on high level models and languages for parallel processing","author":"Michaelson G","year":"2001"},{"key":"p_36","unstructured":"[Nad] Nadathur G Teyjus lambda Prolog. http:\/\/teyjus.cs.umn.edu"},{"key":"p_37","first-page":"810","volume-title":"Kowalski RA, Bowen KA (eds) Logic Programming: Proceedings of the Fifth International Conference and Symposium","author":"Nadathur G","year":"1988"},{"key":"p_38","volume-title":"Isabelle: a generic theorem prover","author":"Pau LC","year":"1994"},{"key":"p_39","volume-title":"ML for the working programmer. CUP","author":"Pau LC","year":"1996","edition":"2"},{"key":"p_40","volume-title":"Structured development of parallel programs","author":"Pel S","year":"1998"},{"key":"p_41","volume-title":"Proceedings of 3rd international conference on principles and practice of declarative programming (PPDP'01)","author":"Pena R","year":"2001"},{"key":"p_42","first-page":"129","volume-title":"Claude Kirchner H\u00e9l\u00e8ne Kirchner (eds) 15th international conference on automated deduction, vol 1421 of Lecture Notes in Artificial Intelligence","author":"Richardson JDC","year":"1998"},{"key":"p_43","first-page":"189","volume-title":"6th International Workshop on High-level parallel programming models and supportive environments","volume":"2026","author":"S\u00e9rot J","year":"2001"},{"key":"p_44","first-page":"49","volume-title":"14th IEEE international conference on automated software engineering, IEEE Computer Society","author":"Stark J","year":"1999"},{"key":"p_45","volume-title":"Foundations of parallel programming. CUP","author":"Ski D","year":"1994"},{"key":"p_46","first-page":"138","volume-title":"Arts T, Mohnen M (eds) Proceedings of 13th International Workshop on the Implementation of Functional Languages, number 2312 in LNCS","author":"Scaife N","year":"2001"},{"key":"p_48","first-page":"31","article-title":"A new implementation technique for applicative languages","volume":"9","author":"Tur DA","year":"1984","journal-title":"Software Pract. Experience"},{"key":"p_49","volume-title":"Programming languages, information structures and machine organisation","author":"Weg P","year":"1979"},{"key":"p_50","unstructured":"[Wic] Wickline P Terzo lambda Prolog. ftp.cis.upenn.edu\/pub\/Terzo"},{"key":"p_51","volume-title":"Austin W (1992) Dynamic control and prototyping of parallel vision algorithms","author":"Wallace A"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0054-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0054-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0054-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:44:41Z","timestamp":1641483881000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0054-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":48,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["10.1007\/s00165-004-0054-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0054-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,5]]}}}