{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:09:44Z","timestamp":1725559784828},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_25","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T19:12:52Z","timestamp":1279653172000},"page":"385-396","source":"Crossref","is-referenced-by-count":8,"title":["Proof Pearl: Defining Functions over Finite Sets"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-24849-1_3","volume-title":"Types for Proofs and Programs","author":"C. Ballarin","year":"2004","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 34\u201350. Springer, Heidelberg (2004)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-54233-7_125","volume-title":"Automata, Languages and Programming","author":"V. Breazu-Tannen","year":"1991","unstructured":"Breazu-Tannen, V., Subrahmanyam, R.: Logical and computational aspects of programming with sets\/bags\/lists. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 60\u201375. Springer, Heidelberg (1991)"},{"key":"25_CR3","unstructured":"Chou, C.-T.: Generalizing an associative and commutative operation with identity to finite sets. HOL88 formal development (1992), ftp:\/\/ftp.cl.cam.ac.uk\/hvg\/hol88\/contrib\/aci\/"},{"key":"25_CR4","volume-title":"Introduction to Lattices and Order","author":"B. Davey","year":"1990","unstructured":"Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)"},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2001","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing\u00a013, 341\u2013363 (2001)","journal-title":"Formal Aspects of Computing"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Gibbons, J., Hutton, G., Altenkirch, T.: When is a Function a Fold or an Unfold?. In: Proc. 4th International Workshop on Coalgebraic Methods in Computer Science. Electronic Notes in Theoretical Computer Science, vol.\u00a044(1) (2001)","DOI":"10.1016\/S1571-0661(04)80906-X"},{"key":"25_CR7","unstructured":"The HOL4 Theorem Prover. http:\/\/hol.sf.net"},{"issue":"4","key":"25_CR8","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1017\/S0956796899003500","volume":"9","author":"G. Hutton","year":"1999","unstructured":"Hutton, G.: A tutorial on the universality and expressiveness of fold. Journal of Functional Programming\u00a09(4), 355\u2013372 (1999)","journal-title":"Journal of Functional Programming"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/67544.66931","volume-title":"Proc. 1989 ACM SIGMOD Intl. Conf. Management of Data","author":"A. Ohori","year":"1989","unstructured":"Ohori, A., Buneman, P., Tannen, V.: Database programming in machiavelli - a polymorphic language with static type inference. In: Clifford, J., Lindsay, B., Maier, D. (eds.) Proc. 1989 ACM SIGMOD Intl. Conf. Management of Data, pp. 46\u201357. ACM Press, New York (1989)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Defining functions on equivalence classes. ACM Transactions on Computational Logic (in press)","DOI":"10.1145\/1183278.1183280"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Organizing numerical theories using axiomatic type classes. Journal of Automated Reasoning (2005) (in press)","DOI":"10.1007\/s10817-004-3997-6"},{"key":"25_CR13","unstructured":"PVS Specification Verification System. http:\/\/pvs.csl.sri.com\/"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11541868_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:18:15Z","timestamp":1605644295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11541868_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}