{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:17:29Z","timestamp":1742995049897,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_21","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"309-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Moessner\u2019s Theorem: An Exercise in Coinductive Reasoning in Coq"],"prefix":"10.1007","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[]},{"given":"Louis","family":"Parlant","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions. In: Texts in TCS. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"21_CR2","unstructured":"Bickford, M., Kozen, D., Silva, A.: Formalizing Moessner\u2019s theorem and generalizations in Nuprl (2013). http:\/\/www.nuprl.org\/documents\/Moessner\/"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1016\/j.tcs.2014.03.012","volume":"546","author":"C Clausen","year":"2014","unstructured":"Clausen, C., Danvy, O., Masuko, M.: A characterization of Moessner\u2019s sieve. Theor. Computut. Sci. 546, 244\u2013256 (2014)","journal-title":"Theor. Computut. Sci."},{"key":"21_CR4","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-1-4612-4072-3_3","volume-title":"The Book of Numbers","author":"John H. Conway","year":"1996","unstructured":"Conway, J.H., Guy, R.K.: Moessner\u2019s magic. In: The Book of Numbers, pp. 63\u201365. Springer, New York (1996)"},{"key":"21_CR5","unstructured":"Coq Development Team: The Coq proof assistant reference manual. INRIA (2013)"},{"key":"21_CR6","unstructured":"Gim\u00e9nez, C.E.: Un Calcul de Constructions Infinies et son Application \u00e0 la v\u00e9rification de syst\u00e8mes communicants. Ph.D. thesis, L\u2019\u00c9cole Normale Sup\u00e9rieure de Lyon (1996)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24452-0_1","volume-title":"Implementation and Application of Functional Languages","author":"R Hinze","year":"2011","unstructured":"Hinze, R.: Scans and convolutions\u2014 a calculational proof of Moessner\u2019s theorem. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol. 5836, pp. 1\u201324. Springer, Heidelberg (2011)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Honsberger, R.: More mathematical morsels. Dolciani Mathematical Expositions. Mathematical Association of America (1991)","DOI":"10.1090\/dol\/010"},{"issue":"2","key":"21_CR9","doi-asserted-by":"publisher","first-page":"131","DOI":"10.4169\/amer.math.monthly.120.02.131","volume":"120","author":"D Kozen","year":"2013","unstructured":"Kozen, D., Silva, A.: On Moessner\u2019s theorem. Am. Math. Monthly 120(2), 131\u2013139 (2013)","journal-title":"Am. Math. Monthly"},{"issue":"8","key":"21_CR10","doi-asserted-by":"publisher","first-page":"846","DOI":"10.2307\/2314178","volume":"73","author":"CT Long","year":"1966","unstructured":"Long, C.T.: On the Moessner theorem on integral powers. Am. Math. Monthly 73(8), 846\u2013851 (1966)","journal-title":"Am. Math. Monthly"},{"issue":"438","key":"21_CR11","doi-asserted-by":"publisher","first-page":"273","DOI":"10.2307\/3615513","volume":"66","author":"CT Long","year":"1982","unstructured":"Long, C.T.: Strike it out-add it up. The Math. Gaz. 66(438), 273\u2013277 (1982)","journal-title":"The Math. Gaz."},{"key":"21_CR12","unstructured":"Moessner, A.: Eine Bemerkung \u00fcber die Potenzen der nat\u00fcrlichen Zahlen. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 1952, no. 29 (1951)"},{"issue":"3","key":"21_CR13","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10990-012-9082-7","volume":"24","author":"M Niqui","year":"2011","unstructured":"Niqui, M., Rutten, J.J.M.M.: A proof of Moessner\u2019s theorem by coinduction. High.-Ord. Symb. Comput. 24(3), 191\u2013206 (2011)","journal-title":"High.-Ord. Symb. Comput."},{"key":"21_CR14","first-page":"1","volume":"1","author":"I Paasche","year":"1953","unstructured":"Paasche, I.: Ein neuer Beweis des moessnerischen Satzes. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 1952 1, 1\u20135 (1953)","journal-title":"Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse 1952"},{"key":"21_CR15","unstructured":"Paasche, I.: Ein zahlentheoretische-logarithmischer Rechenstab. Math. Naturwiss. Unterr. 6, 26\u201328 (1953,1954)"},{"key":"21_CR16","first-page":"263","volume":"12","author":"I Paasche","year":"1954","unstructured":"Paasche, I.: Eine Verallgemeinerung des moessnerschen Satzes. Compositio Mathematica 12, 263\u2013270 (1954)","journal-title":"Compositio Mathematica"},{"key":"21_CR17","first-page":"31","volume":"4","author":"O Perron","year":"1951","unstructured":"Perron, O.: Beweis des Moessnerschen Satzes. Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse 1951 4, 31\u201334 (1951)","journal-title":"Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse 1951"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1017\/S0960129504004517","volume":"15","author":"J Rutten","year":"2005","unstructured":"Rutten, J.: A coinductive calculus of streams. Math. Struct. Comput. Sci. 15, 93\u2013147 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"21_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3\u201380 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR20","first-page":"7","volume":"2","author":"H Sali\u00e9","year":"1952","unstructured":"Sali\u00e9, H.: Bemerkung zu einem Satz von Moessner. Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse 1952 2, 7\u201311 (1952)","journal-title":"Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse 1952"},{"issue":"1","key":"21_CR21","first-page":"41","volume":"2","author":"M Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Form. Reason. 2(1), 41\u201362 (2009)","journal-title":"J. Form. Reason."},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"21_CR23","unstructured":"Urbak, P.: A formal study of Moessner\u2019s sieve, M.Sc. thesis, Aarhus University (2015)"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T12:24:17Z","timestamp":1720787057000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}