{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T19:31:31Z","timestamp":1760297491419},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1989,3,1]],"date-time":"1989-03-01T00:00:00Z","timestamp":604713600000},"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":[[1989,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We formulate a logical description of the functional programming language Miranda. Distinctive features include a full treatment of pattern matching with repeated variables and the characterisation of various (sub-)domains, like the defined natural numbers and finite definite lists, by means of new quantifiers. These quantifiers are introduced by induction rules, and also carry elimination rules. We also discuss the r\u00f4le of fixed point induction and issues of modularisation and scale.<\/jats:p>","DOI":"10.1007\/bf01887213","type":"journal-article","created":{"date-parts":[[2005,7,5]],"date-time":"2005-07-05T06:18:31Z","timestamp":1120544311000},"page":"339-365","source":"Crossref","is-referenced-by-count":8,"title":["A logic for Miranda"],"prefix":"10.1145","volume":"1","author":[{"given":"Simon","family":"Thompson","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Abramsky S.: The Lazy Lambda Calculus. In: Declarative Programming David A. Turner (ed.) Addison Wesley 1989."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alagi\u0107 S and Arbib M. A.: The Design of Well-Structured and Correct Programs Springer Verlag 1978.","DOI":"10.1007\/978-1-4612-6272-5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Barrett G.: Formal Methods Applied to a Floating Point Number System. IEEE Transactions on Software Engineering Vol. 15 No. 5 May 1989.","DOI":"10.1109\/32.24710"},{"key":"e_1_2_1_2_4_2","unstructured":"Bird R. and Wadler P.: An Introduction to Functional Programming Prentice-Hall 1988."},{"key":"e_1_2_1_2_5_2","unstructured":"Hudak P. and Wadler P.: Report on the functional programming language Haskell December 1988. Draft proposed standard for the functional programming language designed by the authors and twelve others."},{"key":"e_1_2_1_2_6_2","unstructured":"Bell J. L. and Machover M.: A Course in Mathematical Logic North-Holland 1977."},{"key":"e_1_2_1_2_7_2","unstructured":"Jones C. B.: Systematic Software Development using VDM Prentice-Hall 1986."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Moggi E.: Categories of partial morphisms and the \u03bb p calculus. In: Category Theory and Computer Programming Lecture Notes in Computer Science 240 Springer Verlag 1985.","DOI":"10.1007\/3-540-17162-2_126"},{"key":"e_1_2_1_2_9_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_10_2","unstructured":"Peyton Jones S.: The Implementation of Functional Programming Languages Prentice Hall International 1987."},{"key":"e_1_2_1_2_11_2","unstructured":"Plotkin G.: Lecture notes on \u2018bottomless\u2019 domains. Lectures delivered at CSLI 1985."},{"key":"e_1_2_1_2_12_2","unstructured":"Plotkin G.: (Towards a) logic for computable functions. Manuscript describing a logic based on \u2018bottomless\u2019 domains 1985."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Scott D. S.: Identity and existence in intuitionistic logic. In: Applications of Sheaves M. P. Fourman C. S. Mulvey and D. S. Scott (eds) Lecture Notes in Mathematics 753 Springer-Verlag 1979.","DOI":"10.1007\/BFb0061839"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Thompson S. J. Laws in Miranda. In: Proc. ACM Conf. on LISP and Functional Programming ACM Press 1986.","DOI":"10.1145\/319838.319839"},{"key":"e_1_2_1_2_15_2","unstructured":"Thompson S. J. Proving properties of functions defined on lawful types Technical Report 37 Computing Laboratory University of Kent at Canterbury 1986. (Revised version to appear in \u201cScience of Computer Programming\u201d)."},{"key":"e_1_2_1_2_16_2","volume-title":"Technical Report 56","author":"Thompson S. J.","year":"1988"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Turner D. A.: Miranda: a non-strict functional language with polymorphic types. In: Functional Programming Languages and Computer Architecture J. -P. Jouannaud (ed.) Springer-Verlag 1985.","DOI":"10.1007\/3-540-15975-4_26"},{"key":"e_1_2_1_2_18_2","unstructured":"Wadler P.: Pattern matching. In: The Implementation of Functional Programming Languages S. Peyton Jones (ed.) Chapter 5 Prentice Hall 1987."},{"key":"e_1_2_1_2_19_2","unstructured":"Wikstrom A.: Functional Programming in Standard ML Prentice-Hall 1987."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01887213.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01887213\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01887213","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:47Z","timestamp":1641482687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01887213"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,3]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1989,3]]}},"alternative-id":["10.1007\/BF01887213"],"URL":"https:\/\/doi.org\/10.1007\/bf01887213","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,3]]}}}