{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:58:00Z","timestamp":1773097080766,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319089171","type":"print"},{"value":"9783319089188","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08918-8_7","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:44:22Z","timestamp":1404279862000},"page":"93-107","source":"Crossref","is-referenced-by-count":2,"title":["Ramsey Theorem as an Intuitionistic Property of Well Founded Relations"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[]},{"given":"Silvia","family":"Steila","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem in formal logic. Proc. London Math. Soc.\u00a030, 264\u2013286 (1930)","journal-title":"Proc. London Math. Soc."},{"key":"7_CR3","unstructured":"Berardi, S., Steila, S.: Ramsey Theorem for pairs as a classical principle in Intuitionistic Arithmetic. Accepted in Types 2013 Postproceedings (2013)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Friedman, H.: Classically and intuitionistically provably recursive functions, vol.\u00a0699 (1978)","DOI":"10.1007\/BFb0103100"},{"key":"7_CR5","unstructured":"Coquand, T.: A direct proof of Ramsey\u2019s Theorem. Author\u2019s website (1994) (revised in 2011)"},{"issue":"2","key":"7_CR6","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1112\/jlms\/s2-47.2.193","volume":"s2-47","author":"W. Veldman","year":"1993","unstructured":"Veldman, W., Bezem, M.: Ramsey\u2019s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society\u00a0s2-47(2), 193\u2013211 (1993)","journal-title":"Journal of the London Mathematical Society"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-32347-8_17","volume-title":"Interactive Theorem Proving","author":"D. Vytiniotis","year":"2012","unstructured":"Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full - adventures in constructive termination. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 250\u2013265. Springer, Heidelberg (2012)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning, 1st edn. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511576430"},{"key":"7_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Proceedings of the 5th GI-Conference on Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings of the 5th GI-Conference on Theoretical Computer Science. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. In: LICS, pp. 192\u2013201. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319613"},{"issue":"2","key":"7_CR11","doi-asserted-by":"publisher","first-page":"268","DOI":"10.2307\/2272972","volume":"37","author":"C. Jockusch","year":"1972","unstructured":"Jockusch, C.: Ramsey\u2019s Theorem and Recursion Theory. J. Symb. Log.\u00a037(2), 268\u2013280 (1972)","journal-title":"J. Symb. Log."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Bellin, G.: Ramsey interpreted: a parametric version of Ramsey\u2019s Theorem. In: AMS (ed.) Logic and Computation: Proceedings of a Symposium held at Carnegie-Mellon University, vol.\u00a0106, pp. 17\u201337 (1990)","DOI":"10.1090\/conm\/106\/1057813"},{"key":"7_CR13","unstructured":"Oliva, P., Powell, T.: A Constructive Interpretation of Ramsey\u2019s Theorem via the Product of Selection Functions. CoRR abs\/1204.5631 (2012)"}],"container-title":["Lecture Notes in Computer Science","Rewriting and Typed Lambda Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08918-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T05:37:02Z","timestamp":1558935422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08918-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089171","9783319089188"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08918-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}