{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:07Z","timestamp":1759639027250,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030930998"},{"type":"electronic","value":"9783030931001"}],"license":[{"start":{"date-parts":[[2021,12,16]],"date-time":"2021-12-16T00:00:00Z","timestamp":1639612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,12,16]],"date-time":"2021-12-16T00:00:00Z","timestamp":1639612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-93100-1_22","type":"book-chapter","created":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T23:02:26Z","timestamp":1639609346000},"page":"346-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Dialectica Logical Principles"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4509-594X","authenticated-orcid":false,"given":"Davide","family":"Trotta","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6495-7405","authenticated-orcid":false,"given":"Matteo","family":"Spadetto","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1078-6970","authenticated-orcid":false,"given":"Valeria","family":"de Paiva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,12,16]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Aschieri, F., Manighetti, M.: On Natural Deduction for Herbrand Constructive logics II: Curry-Howard correspondence for Markov\u2019s Principle in First-Order Logic and Arithmetic. CoRR abs\/1612.05457 (2016)","DOI":"10.2168\/LMCS-12(3:13)2016"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Avigad, J., Feferman, S.: G\u00f6del\u2019s functional (Dialectica) interpretation. In: Handbook of Proof Theory, vol. 137 (February 1999)","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"22_CR3","unstructured":"Frey, J.: Categories of partial equivalence relations as localizations. preprint (2020)"},{"key":"22_CR4","unstructured":"G\u00f6del, K., Feferman, S., et al.: Kurt G\u00f6del: Collected Works: Volume II: Publications 1938\u20131974, vol. 2. Oxford University Press, Oxford (1986)"},{"issue":"3\u20134","key":"22_CR5","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K G\u00f6del","year":"1958","unstructured":"G\u00f6del, K.: \u00dcber eine bisher noch nicht ben\u00fctzte erweiterung des finiten standpunktes. Dialectica 12(3\u20134), 280\u2013287 (1958)","journal-title":"Dialectica"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Herbelin, H.: An intuitionistic logic that proves Markov\u2019s principle. In: 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp. 50\u201356 (2010)","DOI":"10.1109\/LICS.2010.49"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Hofstra, P.: The Dialectica monad and its cousins. Models, Logics Higherdimensional Categories Tribute Work Mih\u00e1ly Makkai 53, 107\u2013139 (2011)","DOI":"10.1090\/crmp\/053\/05"},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1017\/S0305004100057534","volume":"88","author":"J Hyland","year":"1980","unstructured":"Hyland, J., Johnstone, P., Pitts, A.: Tripos theory. Math. Proc. Camb. Phil. Soc. 88, 205\u2013232 (1980)","journal-title":"Math. Proc. Camb. Phil. Soc."},{"key":"22_CR9","unstructured":"Jacobs, B.: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland Publishing Company, Amsterdam (1999)"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"F Lawvere","year":"1969","unstructured":"Lawvere, F.: Adjointness in foundations. Dialectica 23, 281\u2013296 (1969)","journal-title":"Dialectica"},{"key":"22_CR11","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/BFb0080769","volume-title":"Category Theory, Homology Theory and their Applications II","author":"FW Lawvere","year":"1969","unstructured":"Lawvere, F.W.: Diagonal arguments and cartesian closed categories. In: Category Theory, Homology Theory and their Applications II. LNM, vol. 92, pp. 134\u2013145. Springer, Heidelberg (1969). https:\/\/doi.org\/10.1007\/BFb0080769"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Lawvere, F.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) New York Symposium on Application of Categorical Algebra, vol. 2, pp. 1\u201314. American Mathematical Society, Rhode Island (1970)","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Maietti, M., Pasquali, F., Rosolini, G.: Triposes, exact completions, and Hilbert\u2019s $$\\varepsilon $$-operator. Tbilisi Math. J. 10 (2017). https:\/\/doi.org\/10.1515\/tmj-2017-0106","DOI":"10.1515\/tmj-2017-0106"},{"issue":"6","key":"22_CR14","doi-asserted-by":"publisher","first-page":"1089","DOI":"10.1017\/S0960129505004962","volume":"15","author":"ME Maietti","year":"2005","unstructured":"Maietti, M.E.: Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Struct. Comput. Sci. 15(6), 1089\u20131149 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"3","key":"22_CR15","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/s11787-013-0080-2","volume":"7","author":"M Maietti","year":"2013","unstructured":"Maietti, M., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Log. Univers. 7(3), 371\u2013402 (2013)","journal-title":"Log. Univers."},{"key":"22_CR16","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10485-013-9360-5","volume":"23","author":"M Maietti","year":"2013","unstructured":"Maietti, M., Rosolini, G.: Unifying exact completions. Appl. Categ. Structures 23, 43\u201352 (2013)","journal-title":"Appl. Categ. Structures"},{"key":"22_CR17","unstructured":"Manighetti, M.: Computational interpretations of Markov\u2019s principle (2016)"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Moss, S., von Glehn, T.: Dialectica models of type theory. In: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 739\u2013748. Association for Computing Machinery, New York (2018)","DOI":"10.1145\/3209108.3209207"},{"key":"22_CR19","unstructured":"Nemoto, T., Rathjen, M.: The independence of premise rule in intuitionistic set theories (November 2019)"},{"key":"22_CR20","unstructured":"van Oosten, J.: Realizability: An Introduction to its Categorical Side. ISSN, Elsevier Science (2008). https:\/\/books.google.it\/books?id=0Fvvurmr7FsC"},{"key":"22_CR21","first-page":"47","volume":"92","author":"V de Paiva","year":"1989","unstructured":"de Paiva, V.: The Dialectica categories. Categories Comput. Sci. Logic 92, 47\u201362 (1989)","journal-title":"Categories Comput. Sci. Logic"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"P\u00e9drot, P.: A functional functional interpretation. In: CSL-LICS 2014 Science Logic and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (2014)","DOI":"10.1145\/2603088.2603094"},{"key":"22_CR23","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 6, pp. 39-.129. Oxford University Press, Oxford (1995)"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1017\/S096012950200364X","volume":"12","author":"AM Pitts","year":"2002","unstructured":"Pitts, A.M.: Tripos theory in retrospect. Math. Struct. in Comp. Science 12, 265\u2013279 (2002)","journal-title":"Math. Struct. in Comp. Science"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1002\/malq.19940400203","volume":"40","author":"T Shimura","year":"1994","unstructured":"Shimura, T., Kashima, R.: Cut-elimination theorem for the logic of constant domains. Math. Log. Q. 40, 153\u2013172 (1994)","journal-title":"Math. Log. Q."},{"key":"22_CR26","first-page":"1576","volume":"35","author":"D Trotta","year":"2020","unstructured":"Trotta, D.: The existential completion. Theor. Appl. Categories 35, 1576\u20131607 (2020)","journal-title":"Theor. Appl. Categories"},{"key":"22_CR27","unstructured":"Trotta, D., Maietti, M.: Generalized existential completions and their regular and exact completions. Preprint (2021)"},{"key":"22_CR28","unstructured":"Trotta, D., Spadetto, M.: Quantifier completions, choice principles and applications. preprint (2020). https:\/\/arxiv.org\/abs\/2010.09111"},{"key":"22_CR29","doi-asserted-by":"publisher","unstructured":"Trotta, D., Spadetto, M., de Paiva, V.: The G\u00f6del fibration. In: 46th International Symposium on Mathematical Foundations of Computer Science (2021), LIPIcs, vol. 202, pp. 87:1\u201387:16 (2021). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2021.87","DOI":"10.4230\/LIPIcs.MFCS.2021.87"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-93100-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T00:04:52Z","timestamp":1640563492000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-93100-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,16]]},"ISBN":["9783030930998","9783030931001"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-93100-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021,12,16]]},"assertion":[{"value":"16 December 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LFCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logical Foundations of Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Deerfield Beach, FL","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lfcs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lfcs.ws.gc.cuny.edu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"66% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}