{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T22:40:09Z","timestamp":1737067209898,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":93,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433385"},{"type":"electronic","value":"9783540458845"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","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":[[2002]]},"DOI":"10.1007\/3-540-45884-0_5","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T22:06:11Z","timestamp":1180908371000},"page":"78-122","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Theory of Judgments and Derivations"],"prefix":"10.1007","author":[{"given":"Masahiko","family":"Sato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L. and Levy, J.-J., Explicit substitutions, pp. 375\u2013416, Journal of Functional Programming, 1, 1991.","journal-title":"Journal of Functional Programming"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1010051815785","volume":"11","author":"H. Abelson","year":"1998","unstructured":"Abelson, H. et. al, Revised5 report on the algorithmic language scheme, Higherorder and symbolic computation, 11, pp. 7\u2013105, 1998.","journal-title":"Higherorder and symbolic computation"},{"doi-asserted-by":"crossref","unstructured":"Aczel, P., Frege structures and the notions of proposition, truth and set, in Barwsise, J. et al. eds., The Kleene Symposium, North-Holland, Amsterdam, pp. 31\u201350, 1980.","key":"5_CR3","DOI":"10.1016\/S0049-237X(08)71252-7"},{"doi-asserted-by":"crossref","unstructured":"Aczel, P., Carlisle, D.P., Mendler N., Two frameworks of theories and their implementation in Isabelle, pp. 3\u201339, in [38], 1991.","key":"5_CR4","DOI":"10.1017\/CBO9780511569807.003"},{"unstructured":"Barendregt, H. P., The Lambda Calculus,Its Syntax and Semantics, North-Holland, 1981.","key":"5_CR5"},{"unstructured":"Beeson, M.J., Foundations of constructive mathematics, Springer, 1980.","key":"5_CR6"},{"key":"5_CR7","volume-title":"Frege\u2019s Theory of Judgement","author":"D. Bell","year":"1979","unstructured":"Bell, D., Frege\u2019s Theory of Judgement, Clarendon Press, Oxford, 1979."},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1023\/A:1010654904735","volume":"27","author":"M. Bognar","year":"2001","unstructured":"Bognar, M., de Vrijer, R., A calculus of lambda calculus contexts, 27, pp. 29\u201359, J. Automated Reasoning, 2001.","journal-title":"J. Automated Reasoning"},{"key":"5_CR9","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable R.L. et al., Implementing Mathematics with the NuPRL Proof Development System, Prentice-Hall, Englewood Clifs, NJ, 1986."},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T. and Huet, G., The calculus of construction, Information and Computation, 76, pp. 95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0304-3975(97)00150-3","volume":"192","author":"L. Dami","year":"1998","unstructured":"Dami, L., A lambda-calculus for dynamic binding, pp. 201\u2013231, Theoretical Computer Science, 192, 1998.","journal-title":"Theoretical Computer Science"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"D. G. Bruijn de","year":"1972","unstructured":"de Bruijn, D. G., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math. 34, pp. 381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"5_CR13","first-page":"579","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"D. G. Bruijn de","year":"1980","unstructured":"de Bruijn, D. G., A survey of the project AUTOMATH, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 579\u2013606, Academic Press, London, 1980."},{"doi-asserted-by":"crossref","unstructured":"de Bruijn, D. G., A plea for weaker frameworks, pp. 40\u201367, in [38], 1991.","key":"5_CR14","DOI":"10.1017\/CBO9780511569807.004"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A., A formulation of the simple theory of types, J. Symbolic Logic, 5, pp. 56\u201368, 1940.","journal-title":"J. Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"Dybjer, P., Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set theoretic semantics, pp. 280\u2013306, in [38], 1991.","key":"5_CR16","DOI":"10.1017\/CBO9780511569807.012"},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BFb0062852","volume-title":"Algebra and Logic","author":"S. Feferman","year":"1975","unstructured":"Feferman, S., A language and axiom for explicit mathematics, in Crossley J.N. ed., Algebra and Logic, Lecture Notes in Computer Science, 450, pp. 87\u2013139, 1975."},{"doi-asserted-by":"crossref","unstructured":"Feferman, S., Indutively presented systems and the formalization of metamathemaics, in van Dalen, D. et al. eds., Logic Colloquim\u2019 80, North-Holland, Amsterdam, 1982.","key":"5_CR18","DOI":"10.1016\/S0049-237X(09)70506-3"},{"doi-asserted-by":"crossref","unstructured":"Feferman, S., Finitary inductively presented logics, in Ferro R. et al. eds., Logic Colloquim\u2019 88, North-Holland, Amsterdam, 1989.","key":"5_CR19","DOI":"10.1016\/S0049-237X(08)70270-2"},{"key":"5_CR20","volume-title":"Logic and Computation in Philosophy","author":"S. Feferman","year":"1998","unstructured":"Feferman, S., In the Light of Logic, Logic and Computation in Philosophy, Oxford University Press, Oxford, 1998."},{"doi-asserted-by":"crossref","unstructured":"Fiore, M., Plotkin, G., and Turi, D., Abstract syntax and variable binding (extended abstract), in Proc. 14th Symposium on Logic in Computer Science, pp. 193\u2013202, 1999.","key":"5_CR21","DOI":"10.1109\/LICS.1999.782615"},{"key":"5_CR22","first-page":"192","volume":"16","author":"G. Frege","year":"1892","unstructured":"Frege, G., \u00dcber Begri. und Gegenstand, Vierteljahrsschrift f\u00fcr wissenschftliche Philosophie, 16, pp. 192\u2013205, 1892.","journal-title":"Vierteljahrsschrift f\u00fcr wissenschftliche Philosophie"},{"unstructured":"Frege, G., Was ist Funktion?, in Festschrift Ludwig Boltzmann gewindmet zum sechzigsten Geburstage,20. Feburar 1904, Leipzig, pp. 656\u2013666, 1904.","key":"5_CR23"},{"key":"5_CR24","first-page":"175","volume":"39","author":"G. Genzten","year":"1935","unstructured":"Genzten, G., Untersuchungen \u00fcber das logische Schlie\u00dfen, I, Mathematische Zeitschrift, 39, pp. 175\u2013210, 1935, English translation in The collected papers of Gerhard Gentzen, Szabo, M.E. ed., pp. 68\u2013131, North-Holland, Amsterdam, 1969.","journal-title":"Mathematische Zeitschrift"},{"unstructured":"Girard, J-Y., Taylor, P., Lafont, Y., Proofs and Types, Cambridge University Press, 1989.","key":"5_CR25"},{"key":"5_CR26","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, pp. 280\u2013287, 1958.","journal-title":"Dialectica"},{"doi-asserted-by":"crossref","unstructured":"Goodman, N., A theory of constructions equivalent to arithmetic, in Intuitionism and Proof Theory, Kino, Myhill and Vesley, eds., North-Holland, pp. 101\u2013120, 1970.","key":"5_CR27","DOI":"10.1016\/S0049-237X(08)70745-6"},{"doi-asserted-by":"crossref","unstructured":"Goto, S., Program synthesis through G\u00f6del\u2019s interpretation, Lecutre Notes in Computer Science, 75, pp. 302\u2013325, 1978.","key":"5_CR28","DOI":"10.1007\/3-540-09541-1_32"},{"unstructured":"Goto, S., Program synthesis from natural deduction proofs, in Sixth International Joint Conference on Artificial Intelligence (IJCAI-79), pp. 339\u2013341, 1979.","key":"5_CR29"},{"unstructured":"Goto, S., How to formalize traces of computer programs, Jumulage Meeting on Typed Lambda Calculi, Edinbrugh, September, 1989.","key":"5_CR30"},{"key":"5_CR31","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F. and Plotkin, G., A framework for defining logics, Journal of the Association for Computing Machinery, 40, pp. 143\u2013184, 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"unstructured":"Hashimoto, M., Ohori, A., A typed context calculus, Theoretical Computer Science, to appear.","key":"5_CR32"},{"key":"5_CR33","volume-title":"Foundation of Computing","author":"S. Hayashi","year":"1988","unstructured":"Hayashi, S. and Nakano, H., PX: A Computational Logic, Foundation of Computing, The MIT Press, Cambridge, 1988."},{"unstructured":"Heyting, A.K., Intuitionism in mathematics, in Philosophy in the mid-century,a survey, Klibansky, ed., Florence, pp. 101\u2013115, 1958.","key":"5_CR34"},{"key":"5_CR35","first-page":"161","volume-title":"Mathematische Annalen","author":"D. Hilbert","year":"1967","unstructured":"Hilbert, D., \u00dcber das Unendliche, Mathematische Annalen, 95, pp. 161\u2013190, English translation in van Heijenoort, J. ed., From Frege to G\u00f6del: A Source Book in Mathematical Logic, Harvard University Press, Cambridge, MA, 1967."},{"key":"5_CR36","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic,L ambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A., The formulae-as-types notion of construction, in Seldin J.P. and Hindley, J.R. eds., To H.B. Curry: Essays on Combinatory Logic,L ambda Calculus and Formalism, pp. 479\u2013490, Academic Press, London, 1980."},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G., A unification algorithm for typed \u03bb-calculus, Thoretical Computer Science, 1, pp. 27\u201357, 1975.","journal-title":"Thoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Huet, G., and Plotkin, G. eds., Logical Frameworks, Cambridge University Press, 1991.","key":"5_CR38","DOI":"10.1017\/CBO9780511569807"},{"unstructured":"Ida, T., Marin, M., Suzuki, T., Reducing search space in solving higher-order equations, in this volume.","key":"5_CR39"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, S., Consitency of Beeson\u2019s formal system RPS and some related results, in Shinoda, J., Slaman, T.A. and Tugu\u00e9, T. eds., Mathematical Logic and Applications,P roceedings of the Logic Meeting held in Kyoto,1987, Lecture Notes in Mathematics, 1388, Springer, pp. 120\u2013140, 1989.","key":"5_CR40","DOI":"10.1007\/BFb0083667"},{"key":"5_CR41","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S.C. Kleene","year":"1945","unstructured":"Kleene, S.C., On the interpretation of intuitionistic number theory, J. Symbolic Logic, 10, pp. 109\u2013124, 1945.","journal-title":"J. Symbolic Logic"},{"key":"5_CR42","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1111\/j.1746-8361.1958.tb01469.x","volume":"12","author":"G. Kreisel","year":"1958","unstructured":"Kreisel, G., Hilbert\u2019s programme, Dialectica, 12, pp. 346\u2013372, 1958.","journal-title":"Dialectica"},{"doi-asserted-by":"crossref","unstructured":"Kreisel, G., Foundations of Intuitionistic Logic, Nagel, Suppes, Tarski eds, Logic, Methodology and Philosophy of Science, Stanford University Press, pp. 198\u2013210.","key":"5_CR43","DOI":"10.1016\/S0049-237X(09)70587-7"},{"key":"5_CR44","first-page":"95","volume-title":"Lectures on Modern Mathematics","author":"G. Kreisel","year":"1965","unstructured":"Kreisel, G., Mathematical Logic, Saaty ed., Lectures on Modern Mathematics,III, Wiley, New York, pp. 95\u2013195, 1965."},{"doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P., An intuitionistic theory of types: Predicative part, Logic Colloquium\u2019 73, Rose, H.E. and Shepherdson, J.C., Eds, Studies in Logic and Foundation of Mathematics, 80, North-Holland, pp. 73\u2013118, 1975.","key":"5_CR45","DOI":"10.1016\/S0049-237X(08)71945-1"},{"unstructured":"Martin-L\u00f6f, P., Intuitionistic Type Theory, Bibliopolis, 1984.","key":"5_CR46"},{"key":"5_CR47","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF00484985","volume":"73","author":"P. Martin-L\u00f6f","year":"1987","unstructured":"Martin-L\u00f6f, P., Truth of a proposition, evidence of a judgment, validity of a proof, Synthese, 73, pp. 407\u2013420, 1987.","journal-title":"Synthese"},{"doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P., Analytic and synthetic judgments in type theory, Parrini, P. ed., Kant and Contemporary Epistemology, Kluwer Academic Publishers, pp. 87\u201399, 1994.","key":"5_CR48","DOI":"10.1007\/978-94-011-0834-8_5"},{"key":"5_CR49","first-page":"11","volume":"1","author":"P. Martin-L\u00f6f","year":"1996","unstructured":"Martin-L\u00f6f, P., On the meanings of the logical constants and the justifications of the logical laws, Nordic J. of Philosophical Logic, 1, pp. 11\u201360, 1996.","journal-title":"Nordic J. of Philosophical Logic"},{"key":"5_CR50","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1010052222987","volume":"12","author":"I. Mason","year":"1999","unstructured":"Mason, I., Computing with contexts, Higher-Order and Symbolic Computation, 12, pp. 171\u2013201, 1999.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"5_CR51","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"McCarthy, J., Recursive functions of symbolic expressions and their computation by machine, Part I, Comm. ACM, 3, pp. 184\u2013195, 1960.","journal-title":"Comm. ACM"},{"unstructured":"McCarthy, J., et. al, LISP 1.5 programmer\u2019s manual, MIT Press, 1965.","key":"5_CR52"},{"key":"5_CR53","first-page":"499","volume-title":"Handbook of Logic in AI and Logic Programming","author":"G. Nadathur","year":"1998","unstructured":"Nadathur, G., Miller, D., Higher-order logic programming, in Gabbay, D.M. et al. eds., Handbook of Logic in AI and Logic Programming, 5, Clarendon Press, Oxford, pp. 499\u2013590, 1998."},{"key":"5_CR54","doi-asserted-by":"crossref","first-page":"1055","DOI":"10.2977\/prims\/1195164948","volume":"30","author":"S. Nishizaki","year":"1994","unstructured":"Nishizaki, S., Simply typed lambda calculus with first-class environments, Publ. RIMS,Kyoto U., 30, pp. 1055\u20131121, 1994.","journal-title":"Publ. RIMS,Kyoto U"},{"unstructured":"Nordstr\u00f6m, B., Petersson, K. and Smith, J.M., Programming in Martin-L\u00f6f\u2019 s Type Theory, Oxford University Press, 200 pages, 1990.","key":"5_CR55"},{"unstructured":"Okada, M., Ideal concepts, intuitions, and mathematical knowledge acquisitions: Husserl\u2019s and Hilbert\u2019s cases (a preliminary report), in this volume.","key":"5_CR56"},{"key":"5_CR57","volume-title":"Gainen-Taishou Riron no Kousou to sono Tetugakuteki Haikei (Eng. A plan of notion-object theory and its philosophical background)","author":"K. Ono","year":"1989","unstructured":"Ono, K., Gainen-Taishou Riron no Kousou to sono Tetugakuteki Haikei (Eng. A plan of notion-object theory and its philosophical background), Nagoya University Press, Nagoya, 1989."},{"key":"5_CR58","volume-title":"Logic and Computation","author":"L. Paulson","year":"1988","unstructured":"Paulson, L., Logic and Computation, Cambridge University Press, Cambridge, 1988."},{"unstructured":"Pitts, A.M., Some notes on inductive and co-inductive techniques in the semantics of functional programs, Notes Series BRICS-NS-94-5, Department of Computer Science, University of Aarhus, 1994.","key":"5_CR59"},{"key":"5_CR60","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014065","volume-title":"Proceedings of the Second International Conference on Typed Lambda Calculi and Applications,TLCA\u2019 95,Edinburgh","author":"R. Pollack","year":"1995","unstructured":"Pollack, R., A verified type-checker, in Dezani-Ciancaglini, M. and Plotkin, G. eds., Proceedings of the Second International Conference on Typed Lambda Calculi and Applications,TLCA\u2019 95,Edinburgh, Springer-Verlag, Lecture Notes in Computer Science 902, 1995."},{"unstructured":"Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Almquist and Wiksell, Stockholm, 1965.","key":"5_CR61"},{"doi-asserted-by":"crossref","unstructured":"Quine, W.V.O., Mathematical Logic, Harvard University Press, 1951.","key":"5_CR62","DOI":"10.4159\/9780674042469"},{"doi-asserted-by":"crossref","unstructured":"Sands, D., Computing with Contexts-a simple approach, in Proc. Higher-Order Operational Techniques in Semantics,HOOTS II, 16 pages, Electronic Notes in Theoretical Computer Science 10, 1998.","key":"5_CR63","DOI":"10.1016\/S1571-0661(05)80694-2"},{"unstructured":"Sato, M., Towards a mathematical theory of program synthesis, in Sixth International Joint Conference on Artificial Intelligence (IJCAI-79), pp. 757\u2013762, 1979.","key":"5_CR64"},{"unstructured":"Sato, M., and Hagiya, M., Hyperlisp, in de Bakker, van Vliet eds., Algorithmic Languages, North-Holland, pp. 251\u2013269, 1981.","key":"5_CR65"},{"key":"5_CR66","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0304-3975(83)90137-8","volume":"22","author":"M. Sato","year":"1983","unstructured":"Sato, M., Theory of symbolic expressions, I, Theoretical Computer Science, 22, pp. 19\u201355, 1983.","journal-title":"Theoretical Computer Science"},{"key":"5_CR67","doi-asserted-by":"publisher","first-page":"455","DOI":"10.2977\/prims\/1195179055","volume":"21","author":"M. Sato","year":"1985","unstructured":"Sato, M., Theory of symbolic expressions, II, Publ. of Res. Inst. for Math. Sci., Kyoto Univ., 21, pp. 455\u2013540, 1985.","journal-title":"Publ. of Res. Inst. for Math. Sci."},{"doi-asserted-by":"crossref","unstructured":"Sato, M., An abstraction mechanism for symbolic expressions, in V. Lifschitz ed., Artificial Intelligence and Mathematical Theory of Computation (Papers in Honor of John McCarthy), Academic Press, pp. 381\u2013391, 1991.","key":"5_CR68","DOI":"10.1016\/B978-0-12-450010-5.50027-X"},{"key":"5_CR69","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-57887-0_96","volume-title":"Theoretical Aspects of Computer Software","author":"M. Sato","year":"1994","unstructured":"Sato, M., Adding proof objects and inductive definition mechanism to Frege structures, in Ito, T. and Meyer, A. eds., Theoretical Aspects of Computer Software, International Syposium TACS\u201994 Proceedings, Lecture Notes in Computer Science, 789, Springer-Verlag, pp. 179\u2013202, 1994."},{"doi-asserted-by":"crossref","unstructured":"Sato, M., Classical Brouwer-Heyting-Kolmogorov interpretation, in Li, M. Maruoka, A. eds., Algorithmic Learning Theory,8th International Workshop, ALT\u201997, Sendai, Japan, October 1997, Proceedings, Lecture Notes in Artificial Intelligence, 1316, Springer-Verlag, pp. 176\u2013196, 1997.","key":"5_CR70","DOI":"10.1007\/3-540-63577-7_43"},{"key":"5_CR71","first-page":"79","volume":"45","author":"M. Sato","year":"2001","unstructured":"Sato, M., Sakurai, T. and Burstall, R., Explicit environments, Fundamenta Informaticae 45, pp. 79\u2013115, 2001.","journal-title":"Fundamenta Informaticae"},{"key":"5_CR72","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-44716-4_23","volume-title":"Proc. Fifth International Symposium on Functional and Logic Programming (FLOPS)","author":"M. Sato","year":"2001","unstructured":"Sato, M., Sakurai, T. and Kameyama, Y., A simply typed context calculus with first-class environments, in Proc. Fifth International Symposium on Functional and Logic Programming (FLOPS), Lecture Notes in Computer Science, 2024, pp. 359\u2013374, 2001."},{"key":"5_CR73","series-title":"Lect Notes Comput Sci","volume-title":"EuroCAST 2001","author":"M. Sato","year":"2001","unstructured":"Sato, M., Kameyama, Y., Takeuti, I., CAL: A computer assisted system for learning compuation and logic, in EuroCAST 2001, Lecture Notes in Computer Science, 2178, 2001."},{"doi-asserted-by":"crossref","unstructured":"Scott, D., Constructive validity, Symposium on automatic demonstration, Lecture Notes in Mathematics, 125, pp. 237\u2013275, Springer, Berlin, 1969.","key":"5_CR74","DOI":"10.1007\/BFb0060636"},{"key":"5_CR75","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1017\/S0022481200028309","volume":"53","author":"S.G. Simpson","year":"1988","unstructured":"Simpson, S.G., Partial realization of Hilbert\u2019s program, J. Symbolic Logic, 53, pp. 359\u2013394, 1988.","journal-title":"J. Symbolic Logic"},{"unstructured":"Skolem, T., The foundations of elementary arithmetic established by means of the recursive mode of thought, without the use of apparent variables ranging over infinite domains, in [91], pp. 302\u2013333.","key":"5_CR76"},{"doi-asserted-by":"crossref","unstructured":"Smorynski, C., The incompleteness theorems, Barwise, J. ed., Handbook of mathematical logic, Studies in logic and the foundations of mathematics, 90, pp. 821\u2013865, North-Holland, 1977.","key":"5_CR77","DOI":"10.1016\/S0049-237X(08)71123-6"},{"doi-asserted-by":"crossref","unstructured":"Stoyan, H., The influence of the designer on the design-J. McCarthy and LISP, in V. Lifschitz ed., Artificial Intelligence and Mathematical Theory of Computation (Papers in Honor of John McCarthy), Academic Press, pp. 409\u2013426, 1991.","key":"5_CR78","DOI":"10.1016\/B978-0-12-450010-5.50029-3"},{"key":"5_CR79","volume-title":"Annals of Mathematics Studies","author":"R. Smullyan","year":"1961","unstructured":"Smullyan, R., Theory of Formal System, Annals of Mathematics Studies, 47, Princeton University Press, Princeton, 1961."},{"key":"5_CR80","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF00247187","volume":"12","author":"G. Sundholm","year":"1983","unstructured":"Sundholm, G., Constructions, proofs and the meaning of logical constants, J. Phil. Logic, 12, pp. 151\u2013172, 1983.","journal-title":"J. Phil. Logic"},{"key":"5_CR81","doi-asserted-by":"publisher","first-page":"524","DOI":"10.2307\/2026089","volume":"78","author":"W.W. Tait","year":"1981","unstructured":"Tait, W.W., Finitism, J. of Philosophy, 78, pp. 524\u2013546, 1981.","journal-title":"J. of Philosophy"},{"doi-asserted-by":"crossref","unstructured":"Takeuti, G., Generalized Logic Calculus, Journal of Mathematical Society of Japan, 1954.","key":"5_CR82","DOI":"10.4099\/jjm1924.24.0_149"},{"unstructured":"Takeuti, G., Proof Theory, North-Holland, Amsterdam, 1975.","key":"5_CR83"},{"unstructured":"Takeuti, G., A conservative extension of Peano arithmetic, Two Applications of Logic to Mathematics, Part II, Princeton University Press, and Publications of the Mathematical Society of Japan 13, 1978.","key":"5_CR84"},{"key":"5_CR85","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(93)90240-T","volume":"112","author":"C. Talcott","year":"1993","unstructured":"Talcott, C., A Theory of binding structures and applications to rewriting, Theoretical Computer Science, 112, pp. 99\u2013143, 1993.","journal-title":"Theoretical Computer Science"},{"key":"5_CR86","first-page":"309","volume":"90","author":"M. Tatsuta","year":"1991","unstructured":"Tatsuta, M., Program synthesis using realizability, Theoretical Computer Science, 90, pp. 309\u2013353, 1991.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Realizability and functional interpretation, in Troelstra, A.S. ed., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, 344, Springer-Verlag, 1973.","key":"5_CR87","DOI":"10.1007\/BFb0066739"},{"unstructured":"Troelstra, A.S. and van Dalen, D., Constructivism in Mathematics, An Introduction, I, North-Holland, Amsterdam, 1988.","key":"5_CR88"},{"unstructured":"Troelstra, A.S., Schwichtenberg, H., Basic Proof Theory, Cambridge University Press, 1996.","key":"5_CR89"},{"key":"5_CR90","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1142\/S0129054101000400","volume":"12","author":"Y. Tsukada","year":"2001","unstructured":"Tsukada, Y., Martin-L\u00f6f\u2019s type theory as an open-ended framework, International J. of Foundations of Computer Science, 12, pp. 31\u201368, 2001.","journal-title":"International J. of Foundations of Computer Science"},{"key":"5_CR91","volume-title":"From Frege to G\u00f6del,A source Book in Mathematical Logic, 1879\u20131931","author":"J. Heijenoort van","year":"1967","unstructured":"van Heijenoort, J., From Frege to G\u00f6del,A source Book in Mathematical Logic, 1879\u20131931, Harvard University Press, Cambridge, MA, 1967."},{"unstructured":"Voda, P., Theory of pairs, part I: provably recursive functions, Technical Report of Dept. Comput. Science, UBC, Vancouver, 1984.","key":"5_CR92"},{"key":"5_CR93","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BF03037440","volume":"4","author":"P. Voda","year":"1986","unstructured":"Voda, P., Computation of full logic programs using one-variable environments, New Generation Computing, 4, pp. 153\u2013187, 1986.","journal-title":"New Generation Computing"}],"container-title":["Lecture Notes in Computer Science","Progress in Discovery Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45884-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T22:08:34Z","timestamp":1737065314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45884-0_5"}},"subtitle":["Dedicated to the Memory of Professor Katuzi Ono"],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433385","9783540458845"],"references-count":93,"URL":"https:\/\/doi.org\/10.1007\/3-540-45884-0_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"14 March 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}