{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:10Z","timestamp":1763468050182},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540156482"},{"type":"electronic","value":"9783540395270"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_5","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:22:25Z","timestamp":1330176145000},"page":"61-78","source":"Crossref","is-referenced-by-count":19,"title":["Recursive definitions in type theory"],"prefix":"10.1007","author":[{"given":"R. L.","family":"Constable","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N. P.","family":"Mendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","unstructured":"Allen, Stuart. The logical foundations of type theory. (To appear as Cornell Ph.D. thesis.)"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P. An introduction to inductive definitions. Handbook of Mathematical Logic, Barwise, J. (ed.), North Holland, NY (1977) 739\u2013782."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bates, J.L. and Constable, R.L. Proofs as programs. TOPLAS, January 1985.","DOI":"10.1145\/2363.2528"},{"key":"5_CR4","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop, E., Foundations of Constructive Analysis. McGraw Hill, New York, NY, 1967. 370 pp."},{"key":"5_CR5","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S. and Moore, J.S. A Computational Logic. Academic Press, New York, NY, 1979. 397 pp."},{"key":"5_CR6","unstructured":"Brouwer, L.E.J. Collected Works, Vol. 1, A. Heyting, (Ed.), North-Holland, 1975."},{"key":"5_CR7","first-page":"228","volume-title":"User-defined data types as an aid to verifying Lisp programs","author":"R. Cartwright","year":"1976","unstructured":"Cartwright, R. User-defined data types as an aid to verifying Lisp programs. Proc. of the 3rd Int'l. Colloq. on Automata, Languages and Programming, [Michaelson, S. and Milner, R., eds.], Edinburgh University Press, Edinburgh (1976) 228\u2013256."},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/BFb0025773","volume-title":"Logics of Programs","author":"R. Cartwright","year":"1982","unstructured":"Cartwright, R. Toward a logical theory of program data. In Logics of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, New York, NY (1982) 37\u201351."},{"key":"5_CR9","doi-asserted-by":"crossref","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, (1940), 56\u201368.","journal-title":"J. Symbolic Logic"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Constable, Robert L. Constructive mathematics and automatic program writers. In Proc. of IFIP Congress, Ljubljana, 1971, 229\u2013233.","DOI":"10.1136\/bmj.1.5742.233-c"},{"key":"5_CR11","unstructured":"Constable, Robert L. Constructive mathematics as a programming logic I: some principles of theory. Technical report TR83-554, Dept. of Computer Science, Cornell University, May 1983. (To appear in Proc. of FCT Conf., Springer-Verlag, 1983)."},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of 6th G.I. Conference","author":"R. L. Constable","year":"1983","unstructured":"Constable, Robert L. Partial functions in constructive formal theories. In Proc. of 6th G.I. Conference, Lecture Notes in Computer Science 45, Springer-Verlag, New York, NY, 1983."},{"key":"5_CR13","unstructured":"Constable, R.L., and Bates, J.L. The nearly ultimate PRL. Tech. Rep., Dept. of Computer Science, Cornell University, TR 83-551, 1984."},{"key":"5_CR14","volume-title":"A Programming Logic","author":"R. L. Constable","year":"1978","unstructured":"Constable, Robert L. and O'Donnell, M.J. A Programming Logic. Winthrop, Cambridge, 1978."},{"issue":"1","key":"5_CR15","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1145\/357233.357238","volume":"6","author":"R. L. Constable","year":"1984","unstructured":"Constable, Robert L. and Zlatin, D.R. The type theory of PL\/CV3. ACM Trans. on Prog. Lang. & Syst., 6:1 (Jan. 1984) 94\u2013117.","journal-title":"ACM Trans. on Prog. Lang. & Syst."},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","first-page":"116","volume-title":"Proc. of Workshop on Logics of Programs","author":"R. L. Constable","year":"1983","unstructured":"Constable, Robert L. Mathematics as programming. In Proc. of Workshop on Logics of Programs,Lecture Notes in Computer Science 164, Springer-Verlag, New York, NY, 1983, 116\u2013128."},{"key":"5_CR17","volume-title":"Combinatory Logic, Volume II","author":"H.B. Curry","year":"1972","unstructured":"Curry, H.B., Hindley, J.R. and Seldin, J.P. Combinatory Logic, Volume II. North-Holland Publ. Co., Amsterdam, 1972."},{"key":"5_CR18","first-page":"579","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. deBruijn","year":"1980","unstructured":"deBruijn, N.G. A survey of the project AUTOMATH. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.), Academic Press, New York, NY, 1980, 579\u2013607."},{"key":"5_CR19","unstructured":"Demers, A.J. and Donahue, J. Revised report on Russell. Tech. Rep., Department of Computer Science, Cornell University, TR 79-389, September 1979."},{"key":"5_CR20","first-page":"303","volume-title":"Intuitionism and Proof Theory","author":"S. Feferman","year":"1970","unstructured":"Feferman, S. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitionism and Proof Theory, Kino, A., Myhill, J., and Vesley, R.E. (eds.), North Holland, Amsterdam (1970) 303\u2013326."},{"key":"5_CR21","unstructured":"Girard, J.-Y. Interpretation Fonctionelle et Elimination des Coupures de l'arithme\u00e9tique d'ordre sup\u00e9rieur. Ph.D. Thesis, Univ. of Paris VII, 1972."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., and Wadsworth, C. Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"5_CR23","volume-title":"Aspects of the implementations of type theory","author":"R. Harper","year":"1985","unstructured":"Harper, R. Aspects of the implementations of type theory. Ph.D. thesis, Computer Science Department, Cornell University, NY, June 1985."},{"issue":"2","key":"5_CR24","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00976239","volume":"4","author":"C.A.R. Hoare","year":"1975","unstructured":"Hoare, C.A.R. Recursive data structures. International Journal of Computer and Information Sciences, 4:2, (June 1975), 105\u2013132.","journal-title":"International Journal of Computer and Information Sciences"},{"key":"5_CR25","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C. Introduction to Metamathematics. D. Van Nostrand, Princeton, NJ, 1952."},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Kleene, S.C. Formalized recursive functionals and formalized realizability. Memoirs of the American Math. Society, No. 89, 1969.","DOI":"10.1090\/memo\/0089"},{"key":"5_CR27","unstructured":"Kreisel, G. Generalized inductive definitions, section III. Standard report on the foundations of analysis (mimeographed), 1963."},{"key":"5_CR28","volume-title":"The Art of Computer Programming, Vol. I.","author":"D.E. Knuth","year":"1968","unstructured":"Knuth, D.E. The Art of Computer Programming, Vol. I. Addison-Wesley, Reading, 1968."},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"MacQueen, D.B., Plotkin, Gordon D. and Sethi, R. An Ideal Model for Recursive Polymorphic Types. 11th ACM Symp. on Principles of Programming Languages, (1984) 165\u2013174.","DOI":"10.1145\/800017.800528"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"MacQueen, D.B., and Sethi, R. A semantic model of types for applicative languages. ACM Symp. on LISP and Functional Programming, 1982, 243\u2013252.","DOI":"10.1145\/800068.802156"},{"key":"5_CR31","volume-title":"6th International Congress for Logic, Methodology and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, Per. Constructive mathematics and computer programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, North-Holland, Amsterdam, 1982."},{"key":"5_CR32","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0049-237X(08)70847-4","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"P. Martin-L\u00f6f","year":"1971","unstructured":"Martin-L\u00f6f, P. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Proceedings of the Second Scandinavian Logic Symposium, J.E. Fenstad (Ed.), North-Holland, Amsterdam, 1971, 179\u2013216."},{"key":"5_CR33","unstructured":"McCarty, David C. Realizability and recursive mathematics. Computer Science Dept. Tech. Rpt. CMU-CS-84-131, Carnegie-Mellon University (1984)."},{"key":"5_CR34","volume-title":"Algol 68, A First and Second Course","author":"A.D. McGettrick","year":"1978","unstructured":"McGettrick, A.D. Algol 68, A First and Second Course. Cambridge University Press, Cambridge, 1978."},{"key":"5_CR35","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. R. Meyer","year":"1982","unstructured":"Meyer, Albert R. What is a model of the lambda calculus? Information and Control, 52, (1982), 87\u2013122.","journal-title":"Information and Control"},{"key":"5_CR36","volume-title":"Elementary Induction on Abstract Structures","author":"Y. N. Moschovakis","year":"1974","unstructured":"Moschovakis, Yiannis N. Elementary Induction on Abstract Structures. North Holland, London, 1974."},{"key":"5_CR37","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0022-0000(78)90006-5","volume":"17","author":"G. D. Plotkin","year":"1978","unstructured":"Plotkin, Gordon D. Tw as a universal domain. J. Computer and System Sciences, 17, (1978), 209\u2013236.","journal-title":"J. Computer and System Sciences"},{"key":"5_CR38","unstructured":"Plotkin, Gordon D. Private communication."},{"key":"5_CR39","unstructured":"PRL Staff, The. Constructing proofs: An introduction to the Nuprl proof development system. Computer Science Department, Cornell University, January 1985."},{"key":"5_CR40","doi-asserted-by":"crossref","DOI":"10.4159\/9780674042421","volume-title":"Set Theory and Its Logic","author":"W. V. O. Quine","year":"1963","unstructured":"Quine, Willard Van Orman. Set Theory and Its Logic. Harvard University Press, Cambridge, 1963."},{"key":"5_CR41","first-page":"513","volume":"83","author":"J. C. Reynolds","year":"1983","unstructured":"Reynolds, John C. Types, abstraction, and parametric polymorphism. Information Processing 83, IFIP, North Holland Publishers, 1983, 513\u2013523.","journal-title":"Information Processing"},{"key":"5_CR42","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B. Russell","year":"1908","unstructured":"Russell, B. Mathematical logic as based on a theory of types. Am. J. of Math., 30, (1908), 222\u2013262.","journal-title":"Am. J. of Math."},{"issue":"3","key":"5_CR43","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","volume":"5","author":"D. Scott","year":"1976","unstructured":"Scott, Dana. Data types as lattices. SIAM Journal on Computing, 5:3 (September 1976) 522\u2013587.","journal-title":"SIAM Journal on Computing"},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Scott, Dana. The lambda calculus, some models, some philosophy. The Kleene Symposium [eds., J. Barwise, et al.], North-Holland, 1980, 381\u2013421.","DOI":"10.1016\/S0049-237X(08)71262-X"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Scott, Dana. Constructive validity. In Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer-Verlag, 1970, 237\u2013275.","DOI":"10.1007\/BFb0060636"},{"key":"5_CR46","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-94-010-2913-1","volume-title":"Combinators, Lambda-terms, and Proof-Theory","author":"S. Stenlund","year":"1972","unstructured":"Stenlund, S. Combinators, Lambda-terms, and Proof-Theory. D. Reidel, Dordrecht, 1972, 183."},{"key":"5_CR47","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"J. E. Stoy","year":"1977","unstructured":"Stoy, Joseph E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977."},{"issue":"2","key":"5_CR48","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"Tait, William W. Intensional interpretation of functionals of finite type. J Symbolic Logic, 32:2, (June 1967), 198\u2013212.","journal-title":"J Symbolic Logic"},{"key":"5_CR49","volume-title":"From Frege to G\u00f6del: A source book in mathematical logic, 1879\u20131931","author":"J. Heijenoort van","year":"1967","unstructured":"van Heijenoort, Jean. From Frege to G\u00f6del: A source book in mathematical logic, 1879\u20131931, Harvard University Press, Cambridge (1967)."},{"key":"5_CR50","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00265077","volume":"5","author":"A.B.J. Wijngaarden van","year":"1975","unstructured":"van Wijngaarden, A.B.J. et al. Revised report on the algorithmic language ALGO 68. Acta Informatica, 5, (1975), 1\u2013236. (Also a Supplement to ALGO BULLETIN, University of Alberta, 1974.)","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T20:35:31Z","timestamp":1640896531000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]}}}