{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,2]],"date-time":"2025-09-02T10:50:14Z","timestamp":1756810214774,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319559100"},{"type":"electronic","value":"9783319559117"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-55911-7_2","type":"book-chapter","created":{"date-parts":[[2017,3,20]],"date-time":"2017-03-20T14:23:37Z","timestamp":1490019817000},"page":"12-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On Choice Rules in Dependent Type Theory"],"prefix":"10.1007","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,21]]},"reference":[{"key":"2_CR1","unstructured":"Aczel, P., Rathjen, M.: Notes on constructive set theory. Mittag-Leffler Technical Report No. 40 (2001)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-22438-6_7","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Asperti","year":"2011","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita interactive theorem prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 64\u201369. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_7"},{"issue":"2","key":"2_CR3","first-page":"91","volume":"7","author":"A Asperti","year":"2014","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C.: Matita tutorial. J. Formalized Reasoning 7(2), 91\u2013199 (2014)","journal-title":"J. Formalized Reasoning"},{"key":"2_CR4","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science. Springer-Verlag, Heidelberg (2004)"},{"key":"2_CR5","unstructured":"Coq Development Team: The Coq Proof Assistant Reference Manual: Release 8.4pl6. INRIA, Orsay, France, April 2015"},{"key":"2_CR6","unstructured":"Coquand, T.: Metamathematical investigation of a calculus of constructions. In: Odifreddi, P. (ed.) Logic in Computer Science, pp. 91\u2013122. Academic Press (1990)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50\u201366. Springer, Heidelberg (1990). doi: 10.1007\/3-540-52335-9_47"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Hyland, J.M.E.: The effective topos. In: The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981). Studies in Logic and the Foundations of Mathematics, vol. 110, pp. 165\u2013216. North-Holland, New York, Amsterdam (1982)","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"2_CR9","unstructured":"Ishihara, H., Maietti, M., Maschio, S., Streicher, T.: Consistency of the Minimalist Foundation with Church\u2019s thesis and Axiom of Choice. Submitted"},{"key":"2_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0927-0","volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"S Mac Lane","year":"1992","unstructured":"Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer Verlag, New York (1992)"},{"issue":"6","key":"2_CR11","doi-asserted-by":"crossref","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":"2_CR12","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/j.apal.2009.01.006","volume":"160","author":"ME Maietti","year":"2009","unstructured":"Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic 160(3), 319\u2013354 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"17","key":"2_CR13","first-page":"445","volume":"27","author":"ME Maietti","year":"2013","unstructured":"Maietti, M.E., Rosolini, G.: Elementary quotient completion. Theory Appl. Categories 27(17), 445\u2013463 (2013)","journal-title":"Theory Appl. Categories"},{"issue":"3","key":"2_CR14","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/s11787-013-0080-2","volume":"7","author":"ME Maietti","year":"2013","unstructured":"Maietti, M.E., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Log. Univers. 7(3), 371\u2013402 (2013)","journal-title":"Log. Univers."},{"issue":"1","key":"2_CR15","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s10485-013-9360-5","volume":"23","author":"ME Maietti","year":"2015","unstructured":"Maietti, M.E., Rosolini, G.: Unifying exact completions. Appl. Categorical Struct. 23(1), 43\u201352 (2015)","journal-title":"Appl. Categorical Struct."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics. Oxford Logic Guides, vol. 48, pp. 91\u2013114. Oxford University Press (2005)","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"2_CR17","unstructured":"Maietti, M.E., Maschio, S.: An extensional Kleene realizability semantics for the Minimalist Foundation. In: Herbelin, H., Letouzey, P., Sozeau, M. (eds.) 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), vol. 39, pp. 162\u2013186. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2015). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2015\/5496"},{"key":"2_CR18","unstructured":"Maietti, M.E., Maschio, S.: A predicative variant of a realizability tripos for the Minimalist Foundation. IfCoLog J. Logics Appl. (2016). Special Issue Proof Truth Computation"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Maietti, M., Rosolini, G.: Relating quotient completions via categorical logic. In: Probst, D. (ed.) Concepts of Proof in Mathematics, Philosophy, and Computer Science, pp. 229\u2013250. De Gruyter (2016)","DOI":"10.1515\/9781501502620-014"},{"key":"2_CR20","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, Bibliopolis, Naples (1984), June 1980"},{"key":"2_CR21","volume-title":"Programming in Martin L\u00f6f\u2019s Type Theory","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin L\u00f6f\u2019s Type Theory. Clarendon Press, Oxford (1990)"},{"key":"2_CR22","volume-title":"Realizability: An Introduction to its Categorical Side","author":"J Oosten van","year":"2008","unstructured":"van Oosten, J.: Realizability: An Introduction to its Categorical Side. Elsevier, Amsterdam (2008)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Sambin, G., Valentini, S.: Building up a toolbox for Martin-L\u00f6f\u2019s type theory: subset theory. In: Sambin, G., Smith, J. (eds.) Twenty-Five Years of Constructive Type Theory, Proceedings of a Congress held in Venice, October 1995, pp. 221\u2013244. Oxford U. P. (1998)","DOI":"10.1093\/oso\/9780198501275.003.0014"},{"issue":"2","key":"2_CR24","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1016\/0304-3975(92)90021-7","volume":"103","author":"T Streicher","year":"1992","unstructured":"Streicher, T.: Independence of the induction principle and the axiom of choice in the pure calculus of constructions. Theoret. Comput. Sci. 103(2), 395\u2013408 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR25","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction. Studies in Logic and the Foundations of Mathematics, vol. I. North-Holland (1988)"},{"key":"2_CR26","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction. Studies in Logic and the Foundations of Mathematics, vol. II. North-Holland (1988)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-55911-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T18:42:05Z","timestamp":1692729725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-55911-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319559100","9783319559117"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-55911-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}