{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:35:50Z","timestamp":1758706550541,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319084336"},{"type":"electronic","value":"9783319084343"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08434-3_18","type":"book-chapter","created":{"date-parts":[[2014,6,30]],"date-time":"2014-06-30T23:14:35Z","timestamp":1404170075000},"page":"236-251","source":"Crossref","is-referenced-by-count":3,"title":["Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?"],"prefix":"10.1007","author":[{"given":"Marco B.","family":"Caminati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"Kerber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Lange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Rowat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Bergman, C.: Universal Algebra: Fundamentals and Selected Topics. Chapman & Hall Pure and Applied Mathematics. Taylor & Francis (2011)","DOI":"10.1201\/9781439851302"},{"key":"18_CR2","unstructured":"Blanchette, J.C., Paulson, L.C.: Hammering Away. A User\u2019s Guide to Sledgehammer for Isabelle\/HOL (December 5, 2013), \n                    \n                      http:\/\/isabelle.in.tum.de\/dist\/Isabelle2013-2\/doc\/sledgehammer.pdf"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Bowen, J., Gordon, M.: Z and HOL. In: Z User Workshop, Cambridge 1994, pp. 141\u2013167. Springer (1994)","DOI":"10.1007\/978-1-4471-3452-7_9"},{"key":"18_CR4","unstructured":"Caminati, M.B., et al.: Proving soundness of combinatorial Vickrey auctions and generating verified executable code, arXiv:1308.1779 [cs.GT] (2013)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"18_CR6","unstructured":"Klein, G., et al. (eds.): Archive of Formal Proofs (2014), \n                    \n                      http:\/\/afp.sf.net\/\n                    \n                    \n                   (visited on March 14, 2014)"},{"key":"18_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-39320-4_13","volume-title":"Intelligent Computer Mathematics","author":"C. Lange","year":"2013","unstructured":"Lange, C., Caminati, M.B., Kerber, M., Mossakowski, T., Rowat, C., Wenzel, M., Windsteiger, W.: A qualitative comparison of the suitability of four theorem provers for basic auction theory. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 200\u2013215. Springer, Heidelberg (2013)"},{"key":"18_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-39320-4_23","volume-title":"Intelligent Computer Mathematics","author":"C. Lange","year":"2013","unstructured":"Lange, C., Rowat, C., Kerber, M.: The ForMaRE Project \u2013 Formal Mathematical Reasoning in Economics. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 330\u2013334. Springer, Heidelberg (2013), arXiv:1303.4194[cs.CE]"},{"key":"18_CR9","unstructured":"Leinster, T.: Rethinking set theory. arXiv preprint arXiv:1212.6543 (2012)"},{"issue":"4","key":"18_CR10","doi-asserted-by":"publisher","first-page":"1102","DOI":"10.1257\/0022051043004586","volume":"42","author":"E. Maskin","year":"2004","unstructured":"Maskin, E.: The unity of auction theory: Milgrom\u2019s master class. Journal of Economic Literature\u00a042(4), 1102\u20131115 (2004), \n                    \n                      http:\/\/scholar.harvard.edu\/files\/maskin\/files\/unity_of_auction_theory.pdf","journal-title":"Journal of Economic Literature"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/11541868_25","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"2005","unstructured":"Nipkow, T., Paulson, L.C.: Proof pearl: Defining functions over finite sets. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 385\u2013396. Springer, Heidelberg (2005)"},{"issue":"4","key":"18_CR12","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/1183278.1183280","volume":"7","author":"L.C. Paulson","year":"2006","unstructured":"Paulson, L.C.: Defining functions on equivalence classes. ACM Transactions on Computational Logic (TOCL)\u00a07(4), 658\u2013675 (2006)","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set Theory for Verification: I. From Foundations to Functions. Journal of Automated Reasoning\u00a011, 353\u2013389 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR14","unstructured":"Paulson, L.C., et al.: Isabelle\/HOL. A Proof Assistant for Higher-Order Logic (2013)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Simpson, S.G.: Subsystems of second order arithmetic, vol.\u00a01. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511581007"},{"key":"18_CR16","unstructured":"Valentine, S.H., et al.: AZ Patterns Catalogue II-definitions and laws, v0.1 (2004)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08434-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T01:16:54Z","timestamp":1558919814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08434-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319084336","9783319084343"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08434-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}