{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,19]],"date-time":"2026-07-19T18:02:26Z","timestamp":1784484146026,"version":"3.55.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032313478","type":"print"},{"value":"9783032313485","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T00:00:00Z","timestamp":1784505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T00:00:00Z","timestamp":1784505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-3-032-31348-5_11","type":"book-chapter","created":{"date-parts":[[2026,7,19]],"date-time":"2026-07-19T17:29:59Z","timestamp":1784482199000},"page":"162-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Glivenko\u2019s Theorem Underneath Structure"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-4751-1516","authenticated-orcid":false,"given":"Riccardo","family":"Borsetto","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3179-7521","authenticated-orcid":false,"given":"Giulio","family":"Fellin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1297-0579","authenticated-orcid":false,"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2053-1688","authenticated-orcid":false,"given":"Cheng-Syuan","family":"Wan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,20]]},"reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1017\/s0960129501003309","volume":"11","author":"P Aczel","year":"2001","unstructured":"Aczel, P.: The Russell-Prawitz modality. Math. Struct. Comput. Sci. 11(4), 541\u2013554 (2001). https:\/\/doi.org\/10.1017\/s0960129501003309","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20133","key":"11_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.apal.2005.05.016","volume":"137","author":"P Aczel","year":"2006","unstructured":"Aczel, P.: Aspects of general topology in constructive set theory. Ann. Pure Appl. Logic 137(1\u20133), 3\u201329 (2006). https:\/\/doi.org\/10.1016\/j.apal.2005.05.016","journal-title":"Ann. Pure Appl. Logic"},{"key":"11_CR3","unstructured":"Altenkirch, T.: Nuclear \u2014 Agda formalisation (2024). https:\/\/github.com\/txa\/nuclear"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Berg, B.v.d.: A Kuroda-style $$j$$-translation. Arch. Math. Log. 58(5), 627\u2013634 (2019). https:\/\/doi.org\/10.1007\/s00153-018-0656-x","DOI":"10.1007\/s00153-018-0656-x"},{"key":"11_CR5","unstructured":"Borsetto, R.: Glivenko\u2019s theorem underneath structure \u2014 Agda formalisation (2026). https:\/\/github.com\/eapiova\/nuclear"},{"issue":"4","key":"11_CR6","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/s001530200144","volume":"42","author":"R Cignoli","year":"2003","unstructured":"Cignoli, R., Torrens, A.: H\u00e1jek basic fuzzy logic and \u0141ukasiewicz infinite-valued logic. Arch. Math. Log. 42(4), 361\u2013370 (2003). https:\/\/doi.org\/10.1007\/s001530200144","journal-title":"Arch. Math. Log."},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1002\/malq.200310082","volume":"50","author":"R Cignoli","year":"2004","unstructured":"Cignoli, R., Torrens, A.: Glivenko like theorems in natural expansions of BCK-logic. Math. Log. Q. 50, 111\u2013125 (2004). https:\/\/doi.org\/10.1002\/malq.200310082","journal-title":"Math. Log. Q."},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1016\/j.apal.2011.11.002","volume":"163","author":"M Escard\u00f3","year":"2012","unstructured":"Escard\u00f3, M., Oliva, P.: The Peirce translation. Ann. Pure Appl. Logic 163, 681\u2013692 (2012). https:\/\/doi.org\/10.1016\/j.apal.2011.11.002","journal-title":"Ann. Pure Appl. Logic"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Fellin, G., Schuster, P.: A general Glivenko\u2013G\u00f6del theorem for nuclei. In: Sokolova, A. (ed.) Proc. of 37th Conf. on the Mathematical Foundations of Programming Semantics, MFPS 2021, Electronic Proceedings in Theoretical Computer Science, vol.\u00a0351, pp. 51\u201366. Open Publishing Assoc. (2021). https:\/\/doi.org\/10.4204\/eptcs.351.4","DOI":"10.4204\/eptcs.351.4"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1017\/s1755020324000170","volume":"18","author":"G Fellin","year":"2025","unstructured":"Fellin, G., Schuster, P.: Conservation as translation. Rev. Symb. Log. 18(1), 316\u2013348 (2025). https:\/\/doi.org\/10.1017\/s1755020324000170","journal-title":"Rev. Symb. Log."},{"key":"11_CR11","unstructured":"Ferreira, G., Oliva, P., Protin, C.L.: On the various translations between classical, intuitionistic and linear logic. Studia Logica (2024). https:\/\/arxiv.org\/abs\/2409.02249, accepted for publication"},{"key":"11_CR12","unstructured":"Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics, Studies in Logic and the Foundations of Mathematics, vol.\u00a0151. Elsevier (2007)"},{"issue":"4","key":"11_CR13","doi-asserted-by":"publisher","first-page":"1353","DOI":"10.2178\/jsl\/1164060460","volume":"71","author":"N Galatos","year":"2006","unstructured":"Galatos, N., Ono, H.: Glivenko theorems for substructural logics over FL. J. Symb. Log. 71(4), 1353\u20131384 (2006). https:\/\/doi.org\/10.2178\/jsl\/1164060460","journal-title":"J. Symb. Log."},{"issue":"14","key":"11_CR14","first-page":"225","volume":"5","author":"V Glivenko","year":"1928","unstructured":"Glivenko, V.: Sur la logique de M. Brouwer. Acad. Roy. Belg. Bull. Cl. Sci. 5(14), 225\u2013228 (1928)","journal-title":"Brouwer. Acad. Roy. Belg. Bull. Cl. Sci."},{"issue":"15","key":"11_CR15","first-page":"183","volume":"5","author":"V Glivenko","year":"1929","unstructured":"Glivenko, V.: Sur quelques points de la logique de M. Brouwer. Acad. Roy. Belg. Bull. Cl. Sci. 5(15), 183\u2013188 (1929)","journal-title":"Brouwer. Acad. Roy. Belg. Bull. Cl. Sci."},{"issue":"1","key":"11_CR16","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993). https:\/\/doi.org\/10.1145\/138027.138060","journal-title":"J. ACM"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"860","DOI":"10.1016\/j.jpaa.2019.06.014","volume":"224","author":"L Haykazyan","year":"2020","unstructured":"Haykazyan, L.: More on a curious nucleus. J. Pure Appl. Algebra 224, 860\u2013868 (2020). https:\/\/doi.org\/10.1016\/j.jpaa.2019.06.014","journal-title":"J. Pure Appl. Algebra"},{"key":"11_CR18","unstructured":"Johnstone, P.T.: Stone Spaces, Cambridge Studies in Advanced Mathematics, vol.\u00a03. Cambridge University Press (1982)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Vol. 2, Oxford Logic Guides, vol.\u00a044. Clarendon Press (2002)","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Kock, A.: Synthetic Differential Geometry, London Math. Soc. Lecture Note Ser., vol.\u00a0333. Cambridge University Press, 2nd edn. (2006). https:\/\/doi.org\/10.1017\/cbo9780511550812","DOI":"10.1017\/cbo9780511550812"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65, 154\u2013170 (1958). https:\/\/api.semanticscholar.org\/CorpusID:123801856","DOI":"10.1080\/00029890.1958.11989160"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Lambek, J.: On the calculus of syntactic types. In: Jakobson, R. (ed.) Structure of Language and its Mathematical Aspects (1961). https:\/\/api.semanticscholar.org\/CorpusID:118284222","DOI":"10.1090\/psapm\/012\/9972"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Lambek, J.: Some lattice models of bilinear logic. Algebra Universalis 34, 541\u2013550 (1995). https:\/\/api.semanticscholar.org\/CorpusID:119782781","DOI":"10.1007\/BF01181877"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Makkai, M.: Towards a categorical foundation of mathematics. In: Makowsky, J.A., Ravve, E.V. (eds.) Logic Colloquium \u201995. Lecture Notes in Logic, vol.\u00a011, pp. 153\u2013190. Cambridge University Press (1998)","DOI":"10.1007\/978-3-662-22108-2_11"},{"issue":"1","key":"11_CR25","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/s0960129501003450","volume":"12","author":"S Negri","year":"2002","unstructured":"Negri, S.: Continuous domains as formal spaces. Math. Struct. Comput. Sci. 12(1), 19\u201352 (2002). https:\/\/doi.org\/10.1017\/s0960129501003450","journal-title":"Math. Struct. Comput. Sci."},{"key":"11_CR26","unstructured":"Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Chalmers University of Technology (2007)"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Odintsov, S.P.: Logic of classical refutability and class of extensions of minimal logic. Logic Logical Philos. 9(9), 91\u2013107 (2001). https:\/\/doi.org\/10.12775\/llp.2001.006","DOI":"10.12775\/llp.2001.006"},{"issue":"3","key":"11_CR28","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/s11225-004-6043-0","volume":"78","author":"SP Odintsov","year":"2004","unstructured":"Odintsov, S.P.: Negative equivalence of extensions of minimal logic. Stud. Logica. 78(3), 417\u2013442 (2004). https:\/\/doi.org\/10.1007\/s11225-004-6043-0","journal-title":"Stud. Logica."},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Odintsov, S.P.: Constructive Negations and Paraconsistency, Trends in Logic, vol.\u00a026. Kluwer (2008). https:\/\/doi.org\/10.1007\/978-1-4020-6867-6","DOI":"10.1007\/978-1-4020-6867-6"},{"issue":"2","key":"11_CR30","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1016\/j.apal.2009.05.006","volume":"161","author":"H Ono","year":"2009","unstructured":"Ono, H.: Glivenko theorems revisited. Ann. Pure Appl. Log. 161(2), 246\u2013250 (2009). https:\/\/doi.org\/10.1016\/j.apal.2009.05.006","journal-title":"Ann. Pure Appl. Log."},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Paoli, F.: Substructural Logics: A Primer, Trends in Logic, vol.\u00a013. Kluwer (2002). https:\/\/doi.org\/10.1007\/978-94-017-3179-9","DOI":"10.1007\/978-94-017-3179-9"},{"key":"11_CR32","unstructured":"Restall, G.: Substructural Logics. In: Zalta, E.N., Nodelman, U. (eds.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Fall 2024 edn. (2024)"},{"key":"11_CR33","volume-title":"Quantales and their Applications, Pitman Research Notes in Mathematics","author":"KI Rosenthal","year":"1990","unstructured":"Rosenthal, K.I.: Quantales and their Applications, Pitman Research Notes in Mathematics, vol. 234. Longman Scientific & Technical, Essex (1990)"},{"key":"11_CR34","unstructured":"Schellinx, H.: The Noble Art of Linear Decorating. Ph.D. thesis, University of Amsterdam (1994). https:\/\/eprints.illc.uva.nl\/id\/eprint\/1964"},{"issue":"1","key":"11_CR35","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1111\/j.1755-2567.1968.tb00337.x","volume":"34","author":"K Segerberg","year":"1968","unstructured":"Segerberg, K.: Propositional logics related to Heyting\u2019s and Johansson\u2019s. Theoria 34(1), 26\u201361 (1968). https:\/\/doi.org\/10.1111\/j.1755-2567.1968.tb00337.x","journal-title":"Theoria"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Simmons, H.: A framework for topology. In: Macintyre, A., Pacholski, L., Paris, J. (eds.) Logic Colloquium \u201977, Studies in Logic and the Foundations of Mathematics, vol.\u00a096, pp. 239\u2013251. North-Holland, Amsterdam (1978). https:\/\/doi.org\/10.1016\/S0049-237x(08)72007-x","DOI":"10.1016\/S0049-237x(08)72007-x"},{"key":"11_CR37","doi-asserted-by":"publisher","first-page":"2063","DOI":"10.1016\/j.jpaa.2010.02.011","volume":"214","author":"H Simmons","year":"2010","unstructured":"Simmons, H.: A curious nucleus. J. Pure Appl. Algebra 214, 2063\u20132073 (2010). https:\/\/doi.org\/10.1016\/j.jpaa.2010.02.011","journal-title":"J. Pure Appl. Algebra"},{"key":"11_CR38","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034","volume":"31","author":"A Vezzosi","year":"2021","unstructured":"Vezzosi, A., M\u00f6rtberg, A., Abel, A.: Cubical Agda: a dependently typed programming language with univalence and higher inductive types. J. Funct. Program. 31, e8 (2021)","journal-title":"J. Funct. Program."},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Wan, C.S.: Semi-substructural logics \u00e0 la lambek. Electr. Proc. Theor. Comput. Sci. 415, 195\u2013213 (2024). https:\/\/doi.org\/10.4204\/eptcs.415.18","DOI":"10.4204\/eptcs.415.18"}],"container-title":["Lecture Notes in Computer Science","Timeless Machines: Computability Across Eras"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-31348-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,19]],"date-time":"2026-07-19T17:30:00Z","timestamp":1784482200000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-31348-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,20]]},"ISBN":["9783032313478","9783032313485"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-31348-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,20]]},"assertion":[{"value":"20 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CiE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Conference on Computability in Europe","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Trier","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cie2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}