{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T05:17:55Z","timestamp":1761974275207,"version":"build-2065373602"},"publisher-location":"Dordrecht","reference-count":49,"publisher":"Springer Netherlands","isbn-type":[{"type":"print","value":"9789048152018"},{"type":"electronic","value":"9789401721097"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/978-94-017-2109-7_6","type":"book-chapter","created":{"date-parts":[[2013,2,15]],"date-time":"2013-02-15T04:52:40Z","timestamp":1360903960000},"page":"83-92","source":"Crossref","is-referenced-by-count":11,"title":["On Applicative Theories"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"J\u00e4ger","sequence":"first","affiliation":[]},{"given":"Reinhard","family":"Kahle","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Strahm","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Aczel, P., \u2018Frege Structures and the Notion of Proposition, Truth and Set\u2019, in J. Barwise et al. (eds), The Kleene Symposium, North-Holland, 1980, pp. 31\u201359.","DOI":"10.1016\/S0049-237X(08)71252-7"},{"key":"6_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics: Metamathematical Studies","author":"MJ Beeson","year":"1985","unstructured":"Beeson, M. J., Foundations of Constructive Mathematics: Metamathematical Studies, Springer, Berlin, 1985."},{"key":"6_CR3","volume-title":"Bounded Arithmetic","author":"SR Buss","year":"1986","unstructured":"Buss, S. R., Bounded Arithmetic, Bibliopolis, Napoli, 1986."},{"key":"6_CR4","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":"6_CR5","unstructured":"Cantini, A., \u2018On the Computational Content of Weak Applicative Theories with Totality I\u2019, 1996, Preliminary Draft."},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"313","DOI":"10.2307\/2586767","volume":"64","author":"A Cantini","year":"1999","unstructured":"Cantini, A. and Minari, P., \u2018Uniform Inseparability in Explicit Mathematics\u2019, J. Symbolic Logic, 64 (1) (1999), 313\u2013326.","journal-title":"J. Symbolic Logic"},{"key":"6_CR7","doi-asserted-by":"publisher","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. Crossley (ed.), Algebra and Logic, LNM 450, Springer, Berlin, 1975, pp. 87\u2013139."},{"key":"6_CR8","first-page":"95","volume":"19","author":"S Feferman","year":"1975","unstructured":"Feferman, S., \u2018A Theory of Variable Types\u2019, Rev. Colombiana Mat., 19 (1975), 95\u2013105.","journal-title":"Rev. Colombiana Mat"},{"key":"6_CR9","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 et al. (eds), Logic Colloquium \u201878, North-Holland, Amsterdam, 1979, pp. 159\u2013224."},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0049-237X(08)71364-8","volume-title":"The Patras Symposion","author":"S Feferman","year":"1982","unstructured":"Feferman, S., \u2018Iterated Inductive Fixed-Point Theories: Application to Hancock\u2019s Conjecture\u2019, in G. Metakides (ed.), The Patras Symposion, North-Holland, Amsterdam, 1982, pp. 171\u2013196."},{"issue":"2","key":"6_CR11","doi-asserted-by":"publisher","first-page":"364","DOI":"10.2307\/2274509","volume":"53","author":"S Feferman","year":"1988","unstructured":"Feferman, S., \u2018Hilbert\u2019s Program Relativized: Proof-Theoretical and Foundational Studies\u2019, J. Symbolic Logic, 53 (2) (1988), 364\u2013384.","journal-title":"J. Symbolic Logic"},{"key":"6_CR12","first-page":"59","volume-title":"Terni e prospettive della logica e della filosofia della scienza contemporanee","author":"S Feferman","year":"1988","unstructured":"Feferman, S., \u2018Weyl Vindicated: \u201cDas Kontinuum\u201d 70 Years Later\u2019, in Terni e prospettive della logica e della filosofia della scienza contemporanee, CLUEB, Bologna, 1988, pp. 59\u201393."},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1090\/conm\/106\/1057818","volume-title":"Logic and Computation","author":"S Feferman","year":"1990","unstructured":"Feferman, S., \u2018Polymorphic Typed Lambda-Calculi in a Type-Free Axiomatic Framework\u2019, in W. Sieg (ed.), Logic and Computation, Contemp. Math. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 101\u2013136."},{"key":"6_CR14","first-page":"95","volume-title":"Logic from Computer Science","author":"S Feferman","year":"1991","unstructured":"Feferman, S., \u2018Logics for Termination and Correctness of Functional Programs\u2019, in Y. N. Moschovakis (ed.), Logic from Computer Science, MSRI Publications 21, Springer, Berlin, 1991, pp. 95\u2013127."},{"key":"6_CR15","first-page":"195","volume-title":"Proof Theory","author":"S Feferman","year":"1992","unstructured":"Feferman, S., \u2018Logics for Termination and Correctness of Functional programs II: Logics of Strength PRA\u2019, in R. Aczel, H. Simmons, and S. S. Wainer (eds), Proof Theory, Cambridge University Press, Cambridge, 1992, pp. 195\u2013225."},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF01135376","volume":"43","author":"S Feferman","year":"1995","unstructured":"Feferman, S., \u2018Definedness\u2019, Erkenntnis, 43 (1995), 295\u2013320.","journal-title":"Erkenntnis"},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0168-0072(93)90013-4","volume":"65","author":"S Feferman","year":"1993","unstructured":"Feferman, S. and J\u00e4ger, G., \u2018Systems of Explicit Mathematics with Non-Constructive p-Operator. Part I\u2019, Ann. Pure Appl. Logic, 65 (3) (1993), 243\u2013263.","journal-title":"Ann. Pure Appl. Logic"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Feferman, S. and J\u00e4ger, G., \u2018Systems of Explicit Mathematics with Non-Constructive p-Operator. Part II\u2019, Ann. Pure Appl. Logic, 79 (1) (1996).","DOI":"10.1016\/0168-0072(95)00028-3"},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/BFb0091896","volume-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies","author":"S Feferman","year":"1981","unstructured":"Feferman, S. and Sieg, W., \u2018Proof-Theoretic Equivalences Between Classical and Constructive Theories for Analysis\u2019, in W. Buchholz et al. (eds), Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, LNM 897, Springer, Berlin, 1981, pp. 78\u2013142."},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1090\/conm\/106\/1057819","volume":"106","author":"F Ferreira","year":"1990","unstructured":"Ferreira, F., \u2018Polynomial Time Computable Arithmetic\u2019, Contemp. Math., 106 (1990), 137\u2013156.","journal-title":"Contemp. Math"},{"key":"6_CR21","volume-title":"Standardstrukturen f\u00fcr Systeme Expliziter Mathematik","author":"T Glass","year":"1993","unstructured":"Glass, T., Standardstrukturen f\u00fcr Systeme Expliziter Mathematik, PhD Thesis, Westf\u00e4lische Wilhelms-Universit\u00e4t M\u00fcnster, 1993."},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/S0168-0072(96)00005-X","volume":"82","author":"T Glass","year":"1996","unstructured":"Glass, T. and Strahm, T., \u2018Systems of Explicit Mathematics with Non-Constructive p-Operator and Join\u2019, Ann. Pure Appl. Logic, 82 (1996), 193\u2013219.","journal-title":"Ann. Pure Appl. Logic"},{"key":"6_CR23","volume-title":"PX: A Computational Logic","author":"S Hayashi","year":"1988","unstructured":"Hayashi, S. and Nakano, H., PX: A Computational Logic, MIT Press, Cambridge, MA, 1988."},{"key":"6_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-12898-5","volume-title":"Recursion-Theoretic Hierarchies","author":"PG Hinman","year":"1978","unstructured":"Hinman, P. G., Recursion-Theoretic Hierarchies, Springer, Berlin, 1978."},{"key":"6_CR25","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF02023014","volume":"23","author":"G J\u00e4ger","year":"1983","unstructured":"J\u00e4ger, G., \u2018A Well-Ordering Proof for Feferman\u2019s Theory To\u2019, Archiv f\u00fcr mathematische Logik und Grundlagenforschung, 23 (1983), 65\u201377.","journal-title":"Archiv f\u00fcr mathematische Logik und Grundlagenforschung"},{"key":"6_CR26","volume-title":"Theories for Admissible Sets: A Unifying Approach to Proof Theory","author":"G J\u00e4ger","year":"1986","unstructured":"J\u00e4ger, G., Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibliopolis, Napoli, 1986."},{"key":"6_CR27","first-page":"118","volume-title":"Computer Science Logic 87","author":"G J\u00e4ger","year":"1988","unstructured":"J\u00e4ger, G., \u2018Induction in the Elementary Theory of Types and Names\u2019, in E. B\u00f6rger et al. (eds), Computer Science Logic \u201887, LNCS 329, Springer, Berlin, 1988, pp. 118\u2013128."},{"key":"6_CR28","first-page":"117","volume-title":"Logic Colloquium","author":"G J\u00e4ger","year":"1989","unstructured":"J\u00e4ger, G., \u2018Type Theory and Explicit Mathematics\u2019, in H.-D. Ebbinghaus et al. (eds), Logic Colloquium \u201887, North-Holland, Amsterdam, 1989, pp. 117\u2013135."},{"key":"6_CR29","doi-asserted-by":"publisher","first-page":"1142","DOI":"10.2307\/2275630","volume":"62","author":"G J\u00e4ger","year":"1997","unstructured":"J\u00e4ger, G., \u2018Power Types in Explicit Mathematics\u2019, J. Symbolic Logic, 62 (1997), 1142\u20131146.","journal-title":"J. Symbolic Logic"},{"key":"6_CR30","unstructured":"J\u00e4ger, G. and Pohlers, W., \u2018Eine beweistheoretische Untersuchung von (A -CA) + (BI) und verwandter Systeme\u2019, in Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse, 1982, pp. 1\u201328."},{"issue":"2","key":"6_CR31","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0168-0072(94)00037-4","volume":"74","author":"G J\u00e4ger","year":"1995","unstructured":"J\u00e4ger, G. and Strahm, T., \u2018Totality in Applicative Theories\u2019, Ann. Pure Appl. Logic, 74 (2) (1995), 105\u2013120.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"6_CR32","doi-asserted-by":"publisher","first-page":"818","DOI":"10.2307\/2275787","volume":"61","author":"G J\u00e4ger","year":"1996","unstructured":"J\u00e4ger, G. and Strahm, T., \u2018Some Theories with Positive Induction of Ordinal Strength cpw0\u2019, J. Symbolic Logic, 61 (3) (1996), 818\u2013842.","journal-title":"J. Symbolic Logic"},{"key":"6_CR33","unstructured":"J\u00e4ger, G. and Strahm, T., \u2018The Proof-Theoretic Strength of the Suslin Operator in Applicative Theories\u2019, in preparation."},{"key":"6_CR34","volume-title":"Universit\u00e4t Bem","author":"D Jansen","year":"1997","unstructured":"Jansen, D., Ontologische Aspekte expliziter Mathematik, Master\u2019s Thesis, Mathematisches Institut, Universit\u00e4t Bem, 1997."},{"key":"6_CR35","volume-title":"Einbettung des Beweissystems LAMBDA in eine Theorie von Operationen und Zahlen","author":"R Kahle","year":"1992","unstructured":"Kahle, R., Einbettung des Beweissystems LAMBDA in eine Theorie von Operationen und Zahlen, Master\u2019s Thesis, Universit\u00e4t M\u00fcnchen, 1992."},{"key":"6_CR36","unstructured":"Kahle, R., \u2018N-Strictness in Applicative Theories\u2019, Archive for Mathematical Logic,to appear."},{"key":"6_CR37","unstructured":"Kahle, R., \u2018Frege Structures for Partial Applicative Theories\u2019, J. Logic Computation,to appear."},{"key":"6_CR38","volume-title":"Universes over Frege Structures, Tech. Rep. IAM-96-010","author":"R Kahle","year":"1996","unstructured":"Kahle, R., Universes over Frege Structures, Tech. Rep. IAM-96\u2013010, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bern, May 1996."},{"key":"6_CR39","volume-title":"Applicative Theories and Frege Structures","author":"R Kahle","year":"1997","unstructured":"Kahle, R., Applicative Theories and Frege Structures, PhD Thesis, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bem, 1997."},{"key":"6_CR40","volume-title":"Predicative Theories of Types and Names","author":"M Marzetta","year":"1993","unstructured":"Marzetta, M., Predicative Theories of Types and Names, PhD Thesis, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bern, 1993."},{"key":"6_CR41","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s001530050105","volume":"37","author":"M Marzetta","year":"1998","unstructured":"Marzetta, M. and Strahm, T., \u2018The p Quantification Operator in Explicit Mathematics with Universes and Iterated Fixed Point Theories with Ordinals\u2019, Arch. Math. Logic, 37 (1998), 391\u2013413.","journal-title":"Arch. Math. Logic"},{"key":"6_CR42","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF01269876","volume":"34","author":"A Schl\u00fcter","year":"1995","unstructured":"Schl\u00fcter, A., \u2018A Theory of Rules for Enumerated Classes of Functions\u2019, Arch. Math. Logic, 34 (1995), 47\u201363.","journal-title":"Arch. Math. Logic"},{"key":"6_CR43","volume-title":"Theories with Self-Application of Strength PRA, Masters Thesis","author":"T Strahm","year":"1992","unstructured":"Strahm, T., Theories with Self-Application of Strength PRA, Master\u2019s Thesis, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bern, 1992."},{"key":"6_CR44","volume-title":"On the Proof Theory of Applicative Theories","author":"T Strahm","year":"1996","unstructured":"Strahm, T., On the Proof Theory of Applicative Theories, PhD Thesis, Institut f\u00fcr Informatik und angewandte Mathematik, Universit\u00e4t Bern, 1996."},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Strahm, T., \u2018Partial Applicative theories and Explicit Substitutions\u2019, J. Logic Comput., 6 (1) (1996).","DOI":"10.1093\/logcom\/6.1.57"},{"key":"6_CR46","doi-asserted-by":"publisher","first-page":"575","DOI":"10.2307\/2275547","volume":"62","author":"T Strahm","year":"1997","unstructured":"Strahm, T., \u2018Polynomial Time Operations in Explicit Mathematics\u2019, J. Symbolic Logic, 62 (1997), 575\u2013594.","journal-title":"J. Symbolic Logic"},{"key":"6_CR47","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0304-3975(92)90169-G","volume":"104","author":"C Talcott","year":"1992","unstructured":"Talcott, C., \u2018A Theory for Program and Data Type Specification\u2019, Theoret. Comput. Sci., 104 (1992), 129\u2013159.","journal-title":"Theoret. Comput. Sci"},{"key":"6_CR48","volume-title":"Constructivism in Mathematics","author":"A Troelstra","year":"1988","unstructured":"Troelstra, A. and van Dalen, D., Constructivism in Mathematics, Vol. I, North-Holland, Amsterdam, 1988."},{"key":"6_CR49","volume-title":"Constructivism in Mathematics","author":"A Troelstra","year":"1988","unstructured":"Troelstra, A. and van Dalen, D., Constructivism in Mathematics, Vol. II, North-Holland, Amsterdam, 1988."}],"container-title":["Logic and Foundations of Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-017-2109-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T07:28:42Z","timestamp":1557559722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-94-017-2109-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9789048152018","9789401721097"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-94-017-2109-7_6","relation":{},"subject":[],"published":{"date-parts":[[1999]]}}}