{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:22:56Z","timestamp":1755220976248,"version":"3.43.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[1999,3]]},"DOI":"10.1023\/a:1026403603439","type":"journal-article","created":{"date-parts":[[2003,11,6]],"date-time":"2003-11-06T11:45:40Z","timestamp":1068119140000},"page":"215-242","source":"Crossref","is-referenced-by-count":3,"title":["Theories of Types and Names with Positive Stratified Comprehension"],"prefix":"10.1007","volume":"62","author":[{"given":"Pierluigi","family":"Minari","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"205535_CR1","volume-title":"The Lambda Calculus, its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"Barendregt, H. P., The Lambda Calculus, its Syntax and Semantics, revised edition, North Holland, Amsterdam 1984.","edition":"revised edition"},{"key":"205535_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics. Metamathematical Studies","author":"M. J. Beeson","year":"1985","unstructured":"Beeson, M. J., Foundations of Constructive Mathematics. Metamathematical Studies, Springer, Berlin 1985."},{"key":"205535_CR3","volume-title":"Logical Frameworks for Truth and Abstraction","author":"A. Cantini","year":"1996","unstructured":"Cantini, A., Logical Frameworks for Truth and Abstraction, North Holland, Amsterdam 1996."},{"key":"205535_CR4","unstructured":"Cantini, A., \u2018Relating Quine's NF to Feferman's EM\u2019, this volume, 141\u2013162."},{"key":"205535_CR5","unstructured":"Cantini, A., and P. Minari, \u2018Uniform inseparability in explicit mathematics\u2019, to appear The Journal of Symbolic Logic."},{"key":"205535_CR6","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/BFb0062852","volume-title":"Algebra and Logic","author":"S. Feferman","year":"1975","unstructured":"Feferman, S., \u2018A language and axioms for explicit mathematics\u2019, in J. N. Crossley (ed.), Algebra and Logic, Lecture Notes in Mathematics 450, Springer, Berlin 1975, 87\u2013139."},{"key":"205535_CR7","first-page":"159","volume-title":"Logic Colloquium '78","author":"S. Feferman","year":"1979","unstructured":"Feferman, S., \u2018Constructive theories of functions and classes\u2019, in M. Boffa, D. van Dalen and K. Mc Aloon (eds.), Logic Colloquium '78, North Holland, Amsterdam 1979, 159\u2013225."},{"key":"205535_CR8","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0168-0072(93)90013-4","volume":"65","author":"S. Feferman","year":"1993","unstructured":"Feferman, S., and G. J\u00c4ger, \u2018Systems of explicit mathematics with non-constructive \u03bc-operator, part I\u2019, Annals of Pure and Applied Logic 65 (1993), 243\u2013263.","journal-title":"Annals of Pure and Applied Logic"},{"key":"205535_CR9","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0168-0072(95)00028-3","volume":"79","author":"S Feferman","year":"1996","unstructured":"Feferman, S and G. J\u00c4ger, \u2018Systems of explicit mathematics with non-constructive \u03bc-operator, part II\u2019, Annals of Pure and Applied Logic 79 (1996), 37\u201352.","journal-title":"Annals of Pure and Applied Logic"},{"key":"205535_CR10","series-title":"Lecture Notes in Computer Science","first-page":"118","volume-title":"Computer Science Logic '87","author":"G. J\u00c4ger","year":"1987","unstructured":"J\u00c4ger, G., \u2018Induction in the elementary theory of types and names\u2019, in E. B\u00f6rger et al. (eds.), Computer Science Logic '87, Lecture Notes in Computer Science 329, Springer, Berlin 1987, 118\u2013128."},{"key":"205535_CR11","doi-asserted-by":"crossref","first-page":"4","DOI":"10.2307\/2275630","volume":"62","author":"G. J\u00c4ger","year":"1997","unstructured":"J\u00c4ger, G., \u2018Power types in explicit mathematics\u2019, The Journal of Symbolic Logic 62 (1997), 4, 1142\u20131146.","journal-title":"The Journal of Symbolic Logic"},{"key":"205535_CR12","doi-asserted-by":"crossref","unstructured":"J\u00c4ger, G., R. Kahle and T. Strahm, \u2018On applicative theories\u2019, to appear in A. Cantini, E. Casari, P. Minari (eds.), Logic and Foundations of Mathematics, Kluwer, Dordrecht, 1999.","DOI":"10.1007\/978-94-017-2109-7_6"},{"key":"205535_CR13","unstructured":"Jansen, D., Zu den Potenztypen in expliziter Mathematik, Master's thesis, Universit\u00e4t Bern, 1997."},{"key":"205535_CR14","unstructured":"Kahle, R., Applikative Theorien und Frege-Strukturen, Ph. D. dissertation, Universit\u00e4t Bern, 1997."},{"key":"205535_CR15","volume-title":"Lambda-calcul, types et mod\u00e8les","author":"J-L. Krivine","year":"1990","unstructured":"Krivine, J-L., Lambda-calcul, types et mod\u00e8les, Masson, Paris 1990."},{"key":"205535_CR16","doi-asserted-by":"crossref","unstructured":"Marzetta, M., Predicative Theories of Types and Names, Ph. D. dissertation, Universit\u00e4t Bern, 1993.","DOI":"10.1007\/3-540-56992-8_20"},{"key":"205535_CR17","volume-title":"Classical Recursion Theory","author":"P. Odifreddi","year":"1989","unstructured":"Odifreddi, P., Classical Recursion Theory, North Holland, Amsterdam 1989."},{"key":"205535_CR18","unstructured":"Strahm, T., On the Proof Theory of Applicative Structures, Ph. D. dissertation, Universit\u00e4t Bern, 1996."},{"key":"205535_CR19","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0168-0072(89)90019-5","volume":"42","author":"S. Takahashi","year":"1989","unstructured":"Takahashi, S., \u2018Monotone inductive definitions in a constructive theory of functions and classes\u2019, Annals of Pure and Applied Logic 42 (1989), 255\u2013297.","journal-title":"Annals of Pure and Applied Logic"},{"key":"205535_CR20","volume-title":"Constructivism in Mathematics","author":"A. S. Troelstra","year":"1988","unstructured":"Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics (2 volumes), North Holland, Amsterdam, 1988."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026403603439.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1026403603439\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026403603439.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:29:24Z","timestamp":1754630964000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1026403603439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,3]]}},"alternative-id":["205535"],"URL":"https:\/\/doi.org\/10.1023\/a:1026403603439","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}