{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:37:51Z","timestamp":1725457071511},"publisher-location":"Berlin\/Heidelberg","reference-count":11,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540579354"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0032393","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:30:32Z","timestamp":1134282632000},"page":"31-60","source":"Crossref","is-referenced-by-count":2,"title":["A functional system with transfinitely defined types"],"prefix":"10.1007","author":[{"given":"Mariko","family":"Yasugi","sequence":"first","affiliation":[]},{"given":"Susumu","family":"Hayashi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","volume-title":"The lambda calculus","author":"H. P. Barendregt","year":"1981","unstructured":"H. P. Barendregt, The lambda calculus (North-Holland, Amsterdam, 1981)."},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Th. Coquand and G. Huet, Calculus of constructions, Information and Computation 76 (1988), 95\u2013120.","journal-title":"Information and Computation"},{"key":"3_CR3","volume-title":"Proofs and types","author":"J-Y. Girard","year":"1989","unstructured":"J-Y. Girard, P. Taylor and Y. Lafont, Proofs and types (Cambridge University Press, Cambridge, 1989)."},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"325","DOI":"10.2307\/2270450","volume":"31","author":"W. A. Howard","year":"1966","unstructured":"W. A. Howard and G. Kreisel, Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, J. Symbolic Logic 31 (1966), 325\u2013358.","journal-title":"J. Symbolic Logic"},{"key":"3_CR5","volume-title":"Introduction to higher order categorical logic","author":"J. Lambek","year":"1984","unstructured":"J. Lambek and P. J. Scott, Introduction to higher order categorical logic (Cambridge University Press, Cambridge, 1984)."},{"key":"3_CR6","unstructured":"Z. Luo, An extended calculus of constructions (Department of Computer Science, University of Edinburgh, 1990)."},{"key":"3_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4099\/jjm1924.41.0_1","volume":"41","author":"G. Takeuti","year":"1973","unstructured":"G. Takeuti and M. Yasugi, The ordinals of the systems of second order arithmetic with the provably \u0394\n1\n2-comprehension axiom and with the \u0394\n1\n2-comprehension axiom respectively, Japanese J. Math. 41 (1973), 1\u201367.","journal-title":"Japanese J. Math."},{"key":"3_CR8","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1017\/S144678870002437X","volume":"32","author":"M. Yasugi","year":"1982","unstructured":"M. Yasugi, Construction principle and transfinite induction up to \u03b5\n0, J. Austral. Math. Soc. 32 (1982), 24\u201347.","journal-title":"J. Austral. Math. Soc."},{"key":"3_CR9","first-page":"227","volume":"34","author":"M. Yasugi","year":"1985","unstructured":"M. Yasugi, Hyper-principle and the functional structure of ordinal diagrams, Comment. Math. Univ. St. Pauli 34 (1985), 227\u2013263 (the opening part); 35 (1986), 1\u201337 (the concluding part).","journal-title":"Comment. Math. Univ. St. Pauli"},{"key":"3_CR10","unstructured":"M. Yasugi and S. Hayashi, Interpretations of transfinite recursion and parametric abstraction in types, Words, Languages and Combinatorics IIedited by M. Ito and H. Jurgensen (World Scientific Publ., Singapore), to appear."},{"key":"3_CR11","first-page":"392","volume-title":"Lecture Notes in Math. 344","author":"J. I. Zucker","year":"1973","unstructured":"J. I. Zucker, Iterated inductive definitions, trees and ordinals, Metamathematical investigations of intuitionistic arithmetic and analysis, ed. by A. S. Troelstra, Lecture Notes in Math. 344 (Springer-Verlag, Berlin 1973), 392\u2013453."}],"container-title":["Lecture Notes in Computer Science","Logic, Language and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0032393.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:06:29Z","timestamp":1607551589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0032393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540579354"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0032393","relation":{},"subject":[]}}