{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T15:13:38Z","timestamp":1779117218332,"version":"3.51.4"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"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":[[1999,9]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>GUI design isn't simply a matter of putting a nice front-end on a capable program. It requires thought about the way in which people might be expected to use a system, and investigation of the ways that they actually use it. Jape's GUI has been designed to be as simple as possible, so that it will not get in the way of the business of proof. It is designed to be minimal in the information that it displays and the gestures that it requires from the user. In this paper we introduce and give a rationale for the design of Jape's user interface, then note some of its drawbacks.<\/jats:p>","DOI":"10.1007\/s001650050050","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T09:25:39Z","timestamp":1030267539000},"page":"244-271","source":"Crossref","is-referenced-by-count":1,"title":["A Minimal Graphical User Interface for the Jape Proof Calculator"],"prefix":"10.1145","volume":"11","author":[{"given":"Richard","family":"Bornat","sequence":"first","affiliation":[{"name":"Department of Computer Science, Queen Mary and Westfield College, University of London UK, , , , , , UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernard","family":"Sufrin","sequence":"additional","affiliation":[{"name":"Programming Research Group, University of Oxford, Oxford, UK, , , , , , UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_2","volume-title":"Macintosh Human Interface Guidelines","author":"[App90] Apple Computer Inc.","year":"1990"},{"key":"p_3","volume-title":"CSLI","author":"Barwise J.","year":"1993"},{"key":"p_4","first-page":"141","volume":"789","author":"Bertot Y.","year":"1995","journal-title":"Pointing. LNCS"},{"key":"p_5","volume-title":"An Introduction to Functional Programming Prentice-Hall International","author":"Bird R. S.","year":"1991"},{"key":"p_6","volume-title":"The life and times of ded, text display editor","author":"Bornat R.","year":"1989"},{"key":"p_7","volume-title":"Proceedings of the 3rd IJCAI","author":"Darlington J.","year":"1973"},{"key":"p_9","volume-title":"Workshop on Programming for Logic Teaching, Leeds","author":"Dyckhoff R.","year":"1987"},{"key":"p_10","volume-title":": Symbolic Logic","author":"Fitch F. B.","year":"1952"},{"key":"p_11","volume-title":"Computers and Education, 27(1)","author":"Fung P.","year":"1996"},{"key":"p_12","volume-title":"et al.: Proofs and Types","author":"Girard J.-Y.","year":"1989"},{"key":"p_13","volume-title":"Uniform substitution","author":"Gries D.","year":"1998"},{"key":"p_14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3180-9","volume-title":"mural: A Formal Development Support System","author":"Jones C. B.","year":"1991"},{"key":"p_15","volume-title":"Eurographics Workshop on Design, Specification and Verification of Interactive Systems, Springer-Verlag","author":"Merriam N. A.","year":"1996"},{"key":"p_16","volume-title":"The Invisible Computer: Why Good Products Can Fail, the Personal Computer Is So Complex, and Information Appliances Are the Solution","author":"Norman Donald A","year":"1998"},{"key":"p_17","volume-title":"William and Lamming","author":"Newman","year":"1995"},{"key":"p_18","volume-title":"William and Sproull","author":"Newman","year":"1979"},{"key":"p_19","volume-title":"Logic for Computer Science","author":"Reeves S.","year":"1990"},{"key":"p_20","volume-title":"The Carnegie Mellon Proof Tutor","author":"Scheines R.","year":"1993"},{"key":"p_21","volume-title":"Fifth ACM Symposium on Software Development Environments","author":"Th\u00e9ry L.","year":"1992"},{"key":"p_22","volume-title":"User Interface Design","author":"Thimbleby Harold","year":"1990"},{"key":"p_23","volume-title":"Using Z: Specification, Refinement and Proof","author":"Woodcock J.","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050050.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050050\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050050","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:33:34Z","timestamp":1641483214000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050050"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,9]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,9]]}},"alternative-id":["10.1007\/s001650050050"],"URL":"https:\/\/doi.org\/10.1007\/s001650050050","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,9]]}}}