{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:02Z","timestamp":1774837802849,"version":"3.50.1"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1999,7]]},"abstract":"<jats:p>The close relationship between writing programs and proving theorems has frequently been \ncited as an advantage of functional programming languages. We illustrate the interplay \nbetween programming and proving in the development of a program for regular expression \nmatching. The presentation is inspired by Lakatos's method of proofs and refutations in \nwhich the attempt to prove a plausible conjecture leads to a revision not only of the proof, \nbut of the theorem itself. We give a plausible implementation of a regular expression matcher \nthat contains a flaw that is uncovered in an attempt to prove its correctness. The failure of \nthe proof suggests a revision of the specification, rather than a change to the code. We then \nshow that a program meeting the revised specification is nevertheless sufficient to solve the \noriginal problem.<\/jats:p>","DOI":"10.1017\/s0956796899003378","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T09:26:15Z","timestamp":1027761975000},"page":"463-469","source":"Crossref","is-referenced-by-count":18,"title":["Proof-directed debugging"],"prefix":"10.1017","volume":"9","author":[{"given":"ROBERT","family":"HARPER","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[1999,7,1]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796899003378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T15:29:34Z","timestamp":1553873374000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796899003378\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,7]]},"references-count":0,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1999,7]]}},"alternative-id":["S0956796899003378"],"URL":"https:\/\/doi.org\/10.1017\/s0956796899003378","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,7]]}}}