{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:44Z","timestamp":1725456104562},"publisher-location":"Berlin\/Heidelberg","reference-count":16,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354011212X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0025775","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T05:23:41Z","timestamp":1132377821000},"page":"72-93","source":"Crossref","is-referenced-by-count":3,"title":["The type theory of PL\/CV3"],"prefix":"10.1007","author":[{"given":"Robert L.","family":"Constable","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel R.","family":"Zlatin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/S0049-237X(08)71989-X","volume-title":"Logic Colloquium '77","author":"P. Aczel","year":"1978","unstructured":"Aczel, Peter, The Type Theoretic Interpretation of Constructive Set Theory, in Logic Colloquium '77, eds. A. Macintyre, L. Pacholaki, J. Paris; North-Holland Publishing Co., Amsterdam, 1978, pp. 55\u201366."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Cartwright, R., A Constructive Alternative to Axiomatic Data Type Definitions, Computer Science Department TR 80-427, Cornell University, 1980.","DOI":"10.1145\/800087.802789"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Constable, R.L., Programs and Types, in Proceedings of the 21st Annual Symposium on Foundations of Computer Science, Syracuse, N. Y., 1980.","DOI":"10.1109\/SFCS.1980.36"},{"key":"6_CR4","unstructured":"Constable, R.L. and D. Zlatin, Report on the Type Theory (V3) of the Programming Logic PL\/CV3, Technical Report TR 81-454, Computer Science Department, Cornell University."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Constable, R.L., S.D. Johnson, and C.D. Eichenlaub, Introduction to the PL\/CV2 Programming Logic, Department of Computer Science, Cornell University, January 1981.","DOI":"10.1007\/3-540-11492-0"},{"key":"6_CR6","unstructured":"de Bruijn, N.G., A Survey of the Project AUTOMATH, in Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 579\u2013606."},{"key":"6_CR7","first-page":"159","volume":"78","author":"S. Feferman","year":"1979","unstructured":"Feferman, S., Constructive Theories of Functions and Classes, Logic Colloquium 78, North-Holland, Amsterdam, 1979, pp. 159\u2013224.","journal-title":"Logic Colloquium"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Gordon, M., R. Milner, and C. Wadsworth, Edinburgh LCF, A Mechanized Logic of Computation, Lecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"6_CR9","volume-title":"Mathematical Logic","author":"D. Hilbert","year":"1950","unstructured":"Hilbert, D., and W. Ackermann, Mathematical Logic, 2nd edition, trans. Robert E. Luce, Chelsea Pub. Co., New York, 1950.","edition":"2nd edition"},{"issue":"2","key":"6_CR10","doi-asserted-by":"publisher","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, Vol. 4, 2, June, 1975, pp. 105\u2013132.","journal-title":"International Journal of Computer and Information Sciences"},{"key":"6_CR11","volume-title":"A Computer System for Checking Proofs","author":"S. Johnson","year":"1980","unstructured":"Johnson, S., A Computer System for Checking Proofs, Ph.D. thesis, Department of Computer Science, Cornell University, Ithaca, New York, November 1980."},{"key":"6_CR12","first-page":"73","volume-title":"Logic Colloquium '73","author":"P. Martin-L\u00f6f","year":"1975","unstructured":"Martin-L\u00f6f, P., An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73, ed. H.E. Rose, J.C. Shepherdson, North-Holland, Amsterdam, 1975, pp. 73\u2013118."},{"key":"6_CR13","unstructured":"Martin-L\u00f6f, P., Constructive Mathematics and Computer Programming, 6th International Congress for Logic, Method. and Phil. of Science, Hannover, August, 1979."},{"key":"6_CR14","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction, Almqvist and Wiksell, Stokholm, 1965."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Scott, D., Data Types as Lattices, SIAM Journal on Computing, 5, 3, September, 1976.","DOI":"10.1137\/0205037"},{"key":"6_CR16","doi-asserted-by":"crossref","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 pp."}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0025775.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:55:26Z","timestamp":1607532926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0025775"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354011212X"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0025775","relation":{},"subject":[]}}