{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T04:05:01Z","timestamp":1749701101929,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319479576"},{"type":"electronic","value":"9783319479583"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47958-3_13","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T13:40:52Z","timestamp":1475934052000},"page":"229-250","source":"Crossref","is-referenced-by-count":4,"title":["Implementing Cantor\u2019s Paradise"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marina","family":"Lenisa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1016\/S0304-3975(02)00037-3","volume":"2901","author":"F Alessi","year":"2003","unstructured":"Alessi, F., Baldan, P., Honsell, F.: A category of compositional domain-models for separable Stone spaces. Theor. Comput. Sci. 2901, 599\u2013635 (2003)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Abramsky, S.: A Cook\u2019s Tour of the Finitary Non-Well-Founded Sets. CoRR, abs\/1111.7148 (2011). http:\/\/arXiv.org\/abs\/1111.7148","key":"13_CR2"},{"issue":"2","key":"13_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-1(2:1)2005","volume":"1","author":"V Capretta","year":"2005","unstructured":"Capretta, V.: General recursion via coinductive types. Log. Meth. Comput. Sci. 1(2), 1\u201318 (2005)","journal-title":"Log. Meth. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Casinghino, C., Sj\u00f6berg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: POPL 2014, pp. 33\u201345. ACM (2014)","key":"13_CR4","DOI":"10.1145\/2535838.2535883"},{"unstructured":"Development Team: Assistant, The Coq Proof Documentation, system download. http:\/\/coq.inria.fr\/","key":"13_CR5"},{"doi-asserted-by":"crossref","unstructured":"Danielsson, N.A., Hughes, J., Jansson, P., Gibbons, J.: Fast and loose reasoning is morally correct. In: POPL 2006, pp. 206\u2013217. ACM (2006)","key":"13_CR6","DOI":"10.1145\/1111320.1111056"},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"1401","DOI":"10.2307\/2274822","volume":"54","author":"M Forti","year":"1989","unstructured":"Forti, M., Hinnion, R.: The consistency problem for positive comprehension principles. J. Symb. Log. 54, 1401\u20131418 (1989)","journal-title":"J. Symb. Log."},{"key":"13_CR8","volume-title":"Partial Differential Equations and the Calculus of Variations","author":"M Forti","year":"1989","unstructured":"Forti, M., Honsell, F.: Models of self-descriptive set theories. In: Colombini, F., Marino, A., Modica, L., Spagnolo, S. (eds.) Partial Differential Equations and the Calculus of Variations. Birkh\u00e4user, Boston (1989). Dedicated to Ennio De Giorgi on his sixtieth birthday"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-58338-6_82","volume-title":"Mathematical Foundations of Computer Science 1994","author":"M Forti","year":"1994","unstructured":"Forti, M., Honsell, F., Lenisa, M.: Processes and hyperuniverses. In: Pr\u00edvara, I., Rovan, B., Ruzi\u010dka, P. (eds.) MFCS 1994. LNCS, vol. 841, pp. 352\u2013363. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58338-6_82"},{"issue":"1&2","key":"13_CR10","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(95)00087-9","volume":"156","author":"M Forti","year":"1996","unstructured":"Forti, M., Honsell, F.: A general construction of hyperuniverses. Theor. Comput. Sci. 156(1&2), 203\u2013215 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"13_CR11","doi-asserted-by":"crossref","first-page":"17","DOI":"10.2307\/2268437","volume":"15","author":"FB Fitch","year":"1950","unstructured":"Fitch, F.B.: A demonstrably consistent mathematics. J. Symb. Log. 15(1), 17\u201324 (1950)","journal-title":"J. Symb. Log."},{"key":"13_CR12","volume-title":"Symbolic Logic - An Introduction","author":"FB Fitch","year":"1952","unstructured":"Fitch, F.B.: Symbolic Logic - An Introduction. The Ronald Press, New York (1952)"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1006\/inco.1998.2700","volume":"143","author":"J-Y Girard","year":"1998","unstructured":"Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175\u2013204 (1998). doi: 10.1006\/inco.1998.2700","journal-title":"Inf. Comput."},{"key":"13_CR14","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1070\/IM1982v018n01ABEH001382","volume":"18","author":"VN Grishin","year":"1982","unstructured":"Grishin, V.N.: Predicate and set-theoretic calculi based on logics without contractions. Math. USSR Izv. 18, 41\u201359 (1982)","journal-title":"Math. USSR Izv."},{"issue":"1","key":"13_CR15","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM (JACM) 40(1), 143\u2013184 (1993). ACM","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"13_CR16","first-page":"293","volume":"26","author":"F Honsell","year":"2016","unstructured":"Honsell, F., Lenisa, M., Liquori, L., Maksimovic, P., Scagnetto, I.: An open logical framework. JLC 26(1), 293\u2013335 (2016). (First pub. in 2013)","journal-title":"JLC"},{"doi-asserted-by":"crossref","unstructured":"Honsell, F., Liquori, L., Maksimovic, P., Scagnetto, I.: A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. In: LMCS (2016, to appear)","key":"13_CR17","DOI":"10.23638\/LMCS-13(3:2)2017"},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1017\/CBO9780511792588.003","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Rutten, J.: An introduction to (co)algebras and (co)induction. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction, pp. 38\u201399. Cambridge University Press, Cambridge (2011)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction \u2014 CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: twelf\u2014a meta-logical framework. In: Pfenning, F., Sch\u00fcrmann, C. (eds.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48660-7_14"},{"key":"13_CR20","volume-title":"Natural Deduction \u2013 A proof-theoretical Study","author":"D Prawitz","year":"2006","unstructured":"Prawitz, D.: Natural Deduction \u2013 A proof-theoretical Study. Dover Publications, New York (2006)"},{"unstructured":"The Twelf Project. http:\/\/twelf.org\/wiki\/Totality_assertion","key":"13_CR21"},{"doi-asserted-by":"crossref","unstructured":"Wang, Y., Nadathur, G.: Towards extracting explicit proofs from totality checking in twelf. In: LFMTP 2013, pp. 55\u201366. ACM (2013)","key":"13_CR22","DOI":"10.1145\/2503887.2503893"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-24849-1_23","volume-title":"Types for Proofs and Programs","author":"K Watkins","year":"2004","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: the propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 355\u2013377. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24849-1_23"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47958-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T03:42:17Z","timestamp":1749613337000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}