{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:32Z","timestamp":1774837832229,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540133469","type":"print"},{"value":"9783540388913","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1984]]},"DOI":"10.1007\/3-540-13346-1_10","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:04:41Z","timestamp":1330175081000},"page":"197-214","source":"Crossref","is-referenced-by-count":5,"title":["Deriving structural induction in LCF"],"prefix":"10.1007","author":[{"given":"Lawrence","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"10_CR1","unstructured":"R. Bird, Programs and Machines: An Introduction to the Theory of Computation, (Wiley, 1976)."},{"key":"10_CR2","unstructured":"W.H. Burge, Recursive Programming Techniques, (Addison-Wesley, 1975)."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"R.M. Burstall, Proving properties of programs by structural induction, Computer Journal 12 (February 1969), pages 41\u201348.","DOI":"10.1093\/comjnl\/12.1.41"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"R.M. Burstall and J.A. Goguen, Algebras, theories and freeness: an introduction for computer scientists, Report CSR-101-82, University of Edinburgh, 1982.","DOI":"10.1007\/978-94-009-7893-5_11"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"R. Cartwright and J. Donahue, The semantics of lazy (and industrious) evaluation, ACM Symposium on Lisp and Functional Programming (1982), pages 253\u2013264.","DOI":"10.1145\/800068.802157"},{"key":"10_CR6","unstructured":"A.J. Cohn and R. Milner, On using Edinburgh LCF to prove the correctness of a parsing algorithm, Report CSR-113-82, University of Edinburgh, 1982."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF (Springer, 1979).","DOI":"10.1007\/3-540-09724-4"},{"key":"10_CR8","unstructured":"S. Igarashi, Admissibility of fixed-point induction in first order logic of typed theories, Report STAN-CS-72-287, Stanford University, 1972."},{"key":"10_CR9","unstructured":"Z. Manna, Mathematical Theory of Computation (McGraw-Hill, 1974)."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"B. Nordstr\u00f6m, Programming in constructive set theory: some examples, ACM conference on Functional Programming Languages and Computer Architecture (1981), pages 141\u2013153.","DOI":"10.1145\/800223.806773"},{"key":"10_CR11","unstructured":"L. Paulson, The revised logic PPLAMBDA: a reference manual, Report 36, Computer Laboratory, University of Cambridge (1983)."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"L. Paulson, Structural induction in LCF, Report 44, Computer Laboratory, University of Cambridge (1984).","DOI":"10.1007\/3-540-13346-1_10"},{"key":"10_CR13","unstructured":"L. Paulson, Verifying the unification algorithm in LCF, Report 50, Computer Laboratory, University of Cambridge (1984)."},{"key":"10_CR14","unstructured":"D. Scott, A type-theoretic alternative to CUCH, ISWIM, OWHY, Unpublished (1969)."},{"key":"10_CR15","unstructured":"S. Sokolowski, An LCF proof of the soundness of Hoare's logic, Report CSR-146-83, University of Edinburgh, 1983."},{"key":"10_CR16","unstructured":"J.E. Stoy, Denotational Semantics: the Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977."}],"container-title":["Lecture Notes in Computer Science","Semantics of Data Types"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-13346-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:07:21Z","timestamp":1605625641000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-13346-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9783540133469","9783540388913"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-13346-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1984]]}}}