{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T20:45:29Z","timestamp":1780778729078,"version":"3.54.1"},"reference-count":9,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1995,7,1]],"date-time":"1995-07-01T00:00:00Z","timestamp":804556800000},"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":[[1995,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper expands upon work begun in [Tho89], in building a logic for the Miranda functional programming language. After summarising the work in that paper, a translation of Miranda definitions into logical formulas is presented, and illustrated by means of examples. This work expands upon [Tho89] in giving a complete treatment of sequences of equations, and by examining how to translate the local definitions introduced by where clauses.<\/jats:p>\n          <jats:p>The status of the logic is then examined, and it is argued that the logic extends a natural operational semantics of Miranda, given by the translations of definitions into conditional equations.<\/jats:p>\n          <jats:p>Finally it is shown how the logic can be implemented in the Isabelle proof tool.<\/jats:p>","DOI":"10.1007\/bf01211216","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:16Z","timestamp":1109369896000},"page":"412-429","source":"Crossref","is-referenced-by-count":3,"title":["A logic for Miranda, revisited"],"prefix":"10.1145","volume":"7","author":[{"given":"Simon","family":"Thompson","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Hudak P. Peyton Jones S. and Wadler P.: (Editors). Report on the Programming Language Haskell version 1.2. ACM SIGPLAN Notices 27(5) 1992.","DOI":"10.1145\/130697.130699"},{"key":"e_1_2_1_2_2_2","unstructured":"Klop. J. W.: Term rewriting systems. In Samson Abramsky Tom Maibaum and Dov Gabbay editors Handbook of Logic in Computer Science Volume II . Oxford University Press 1993."},{"key":"e_1_2_1_2_3_2","unstructured":"Milner R. Tofte M. and Harper R.: The Definition of Standard ML . MIT Press 1990."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Paulson L. C.: Logic and Computation \u2014 Interactive proof with Cambridge LCF . Cambridge University Press 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"e_1_2_1_2_5_2","unstructured":"Paulson L. C: Isabelle: the next 700 theorem provers. In P. Oddifreddi editor Logic and Computer Science . Academic Press 1990."},{"key":"e_1_2_1_2_6_2","unstructured":"Peyton Jones S.: The Implementation of Functional Programming Languages . Prentice Hall International 1987."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Thompson S. J.: A Logic for Miranda. Formal Aspects of Computing 1 1989.","DOI":"10.1007\/BF01887213"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Thompson S. J.: Formulating Haskell. In Workshop on Functional Programming Ayr 1992 Workshops in Computing. Springer Verlag 1993.","DOI":"10.1007\/978-1-4471-3215-8_23"},{"key":"e_1_2_1_2_9_2","unstructured":"Turner D. A.: An overview of Miranda. In David A. Turner editor Research Topics in Functional Programming . Addison Wesley 1990."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211216.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211216\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:56Z","timestamp":1641482696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,7]]},"references-count":9,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,7]]}},"alternative-id":["10.1007\/BF01211216"],"URL":"https:\/\/doi.org\/10.1007\/bf01211216","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,7]]}}}