{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:44Z","timestamp":1725663404957},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540176602"},{"type":"electronic","value":"9783540477464"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/3-540-17660-8_62","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:16:47Z","timestamp":1330197407000},"page":"276-286","source":"Crossref","is-referenced-by-count":5,"title":["Induction principles formalized in the calculus of constructions"],"prefix":"10.1007","author":[{"given":"G\u00e9rard","family":"Huet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"unstructured":"R. Boyer, J Moore. \u201cA Computational Logic.\u201d Academic Press (1979).","key":"20_CR1"},{"unstructured":"N.G. de Bruijn. \u201cAutomath a language for mathematics.\u201d Les Presses de l'Universit\u00e9 de Montr\u00e9al, (1973).","key":"20_CR2"},{"unstructured":"N.G. de Bruijn. \u201cA survey of the project Automath.\u201d (1980) in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds Seldin J. P. and Hindley J. R., Academic Press (1980).","key":"20_CR3"},{"key":"20_CR4","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R. Burstall","year":"1969","unstructured":"R. Burstall. \u201cProving Properties of Programs by Structural Induction.\u201d Comp. J. 12 (1969), 41\u201348.","journal-title":"Comp. J."},{"unstructured":"P. M. Cohn. \u201cUniversal Algebra.\u201d Reidel, 1965.","key":"20_CR5"},{"doi-asserted-by":"crossref","unstructured":"R.L. Constable, N.P. Mendler. \u201cRecursive Definitions in Type Theory.\u201d Private Communication (1985).","key":"20_CR6","DOI":"10.1007\/3-540-15648-8_5"},{"unstructured":"Th. Coquand. \u201cUne th\u00e9orie des constructions.\u201d Th\u00e8se de troisi\u00e8me cycle, Universit\u00e9 Paris VII, Janvier 85.","key":"20_CR7"},{"unstructured":"Th. Coquand. \u201cAn analysis of Girard's paradox.\u201d First IEEE Symposium on Logic in Computer Science, Boston (June 1986), 227\u2013236.","key":"20_CR8"},{"unstructured":"Th. Coquand and G. Huet. \u201cConstructions: A Higher Order Proof System for Mechanizing Mathematics.\u201d EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).","key":"20_CR9"},{"unstructured":"Th. Coquand and G. Huet. \u201cThe Calculus of Constructions.\u201d To appear, Information and Control.","key":"20_CR10"},{"unstructured":"Th. Coquand and G. Huet. \u201cConcepts Math\u00e9matiques et Informatiques Formalis\u00e9s dans le Calcul des Constructions.\u201d Logic Colloquium, Orsay (July 85). To appear, North-Holland.","key":"20_CR11"},{"unstructured":"J.Y. Girard. \u201cInterpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure.\u201d Th\u00e8se d'Etat, Universit\u00e9 Paris VII (1972).","key":"20_CR12"},{"doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner and C. Wadsworth. \u201cEdinburgh LCF.\u201d Springer-Verlag LNCS 78 (1979).","key":"20_CR13","DOI":"10.1007\/3-540-09724-4"},{"unstructured":"P. Martin-L\u00f6f. \u201cA theory of types.\u201d Report 71-3, Dept. of Mathematics, University of Stockholm, Feb. 1971, revised (Oct. 1971).","key":"20_CR14"},{"unstructured":"N.P. Mendler. \u201cFirst and Second-Order Lambda Calculi with Recursive Types.\u201d Technical Report TR 86-764, Dept. of Computer Science, Cornell University (July 1986).","key":"20_CR15"},{"unstructured":"D. Park. \u201cFixpoint Induction and Proofs of Program Properties.\u201d Machine Intelligence 5, Eds. B. Meltzer & D. Michie, 59\u201377, Edinburgh University Press.","key":"20_CR16"},{"unstructured":"L. C. Paulson. \u201cConstructing Recursion Operators in Intuitionistic Type Theory.\u201d Tech. Report 57, Computer Laboratory, University of Cambridge (Oct. 1984). To appear, J. of Symbolic Computation.","key":"20_CR17"},{"doi-asserted-by":"crossref","unstructured":"D. Scott. \u201cConstructive validity.\u201d Symposium on Automatic Demonstration, Springer-Verlag Lecture Notes in Mathematics, 125 (1970).","key":"20_CR18","DOI":"10.1007\/BFb0060636"},{"key":"20_CR19","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1137\/0205037","volume":"5","author":"D. Scott","year":"1976","unstructured":"D. Scott. \u201cData Types as Lattices.\u201d SIAM Journal of Computing 5 (1976) 522\u2013587.","journal-title":"SIAM Journal of Computing"},{"key":"20_CR20","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski. \u201cA Lattice-Theoretical Fixpoint Theorem and its Applications.\u201d Pacific J. Math. 5 (1955), 285\u2013309.","journal-title":"Pacific J. Math."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '87"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-17660-8_62.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:13:15Z","timestamp":1605643995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-17660-8_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540176602","9783540477464"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-17660-8_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1987]]}}}