{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:06Z","timestamp":1779836706430,"version":"3.53.1"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"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,3]]},"abstract":"<jats:p>\n                    The design of theorem provers, especially in the LCF-prover family, has strongly profited \nfrom functional programming. This paper attempts to develop a metaphor suited to visualize \nthe LCF-style prover design, and a methodology for the implementation of graphical user \ninterfaces for these provers and encapsulations of formal methods. In this problem domain, \nparticular attention has to be paid to the need to construct a variety of objects, keep track \nof their interdependencies and provide support for their reconstruction as a consequence of \nchanges. We present a prototypical implementation of a\n                    <jats:italic>generic<\/jats:italic>\n                    and\n                    <jats:italic>open<\/jats:italic>\n                    interface system \narchitecture, and show how it can be instantiated to an interface for Isabelle, called\n                    <jats:bold>IsaWin<\/jats:bold>\n                    , \nas well as to a tailored tool for transformational program development, called\n                    <jats:bold>TAS<\/jats:bold>\n                    .\n                  <\/jats:p>","DOI":"10.1017\/s0956796899003421","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T09:26:15Z","timestamp":1027761975000},"page":"167-189","source":"Crossref","is-referenced-by-count":11,"title":["Functional design and implementation of \ngraphical user interfaces for theorem provers"],"prefix":"10.1017","volume":"9","author":[{"given":"C.","family":"L\u00dcTH","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"B.","family":"WOLFF","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[1999,3,1]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796899003421","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:34:51Z","timestamp":1779834891000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796899003421\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,3]]}},"alternative-id":["S0956796899003421"],"URL":"https:\/\/doi.org\/10.1017\/s0956796899003421","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}