{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:59:53Z","timestamp":1725663593273},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_48","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:45:41Z","timestamp":1330209941000},"page":"226-243","source":"Crossref","is-referenced-by-count":1,"title":["Type theory as a foundation for computer science"],"prefix":"10.1007","author":[{"given":"Robert L.","family":"Constable","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"11_CR1","unstructured":"S. F. Allen. A non-type-theoretic semantics for type-theoretic language. PhD thesis, Cornell University, 1987."},{"key":"11_CR2","unstructured":"S. F. Allen. A non-type-theoretic definition of martin-l\u00f6f's types. Proc. of Second Symp. on Logics in Computer Science, IEEE, pages 215\u2013224., June 1987."},{"key":"11_CR3","volume-title":"Sixth Symp. on Logic in Computer Science, IEEE","author":"P. Audebaud","year":"1991","unstructured":"P. Audebaud. Partial objects in the calculus of constructions. In Sixth Symp. on Logic in Computer Science, IEEE, Vrije University, Amsterdam, The Netherlands, 1991."},{"key":"11_CR4","unstructured":"D. Basin and R. Constable. Meta-logical frameworks. In Proc. of the Second Workshop on Logical Frameworks, Edinburgh, UK, June 1991."},{"key":"11_CR5","unstructured":"J. L. Bates. A logic for correct program development. PhD thesis, Cornell University, 1979."},{"key":"11_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61667-9","volume-title":"Constructive Analysis","author":"E. Bishop","year":"1985","unstructured":"E. Bishop and D. Bridges. Constructive Analysis. NY:Springer-Verlag, 1985."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"W. Buchholtz et al. Iterated inductive definitions and subsystems of analysis. Recent Proof-Theoretical Studies, Lecture Notes in Mathematics, 897, 1981.","DOI":"10.1007\/BFb0091894"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"R. Constable and N. Mendler. Recursive Definitions in Type Theory. In Proc. of Logics of Prog. Conf., pages 61\u201378, January 1985. Cornell TR 85-659.","DOI":"10.1007\/3-540-15648-8_5"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"R. Constable and S. F. Smith. Computational foundations of basic function theory. In Third Symp. on Logic in Somp. Sci. IEEE, 1988. (Cornell TR 88\u2013904).","DOI":"10.1109\/LICS.1988.5133"},{"key":"11_CR10","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Development System. NJ:Prentice-Hall, 1986."},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of construction. Information and Computation, 76:95\u2013120., 1988.","journal-title":"Information and Computation"},{"key":"11_CR12","first-page":"303","volume-title":"Proc. Conf. Intuitionism and Proof Theory","author":"S. Feferman","year":"1970","unstructured":"S. Feferman. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In Proc. Conf. Intuitionism and Proof Theory, pages 303\u2013326, Buffalo, NY, 1970. North-Holland."},{"key":"11_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0049-237X(08)70843-7","volume-title":"2nd Scandinavian Logic Symp.","author":"J.-Y. Girard","year":"1971","unstructured":"J.-Y. Girard. Une extension de l'interpretation de godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In 2nd Scandinavian Logic Symp., pages 63\u201369. NY:Springer-Verlag, 1971."},{"key":"11_CR14","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1988."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: a mechanized logic of computation. Lecture Notes in Computer Science, 78, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"T. Griffin. A formulas-as-types notion of control. In POPL, 1990.","DOI":"10.1145\/96709.96714"},{"key":"11_CR17","volume-title":"PX: A Computational Logic","author":"S. Hayashi","year":"1988","unstructured":"S. Hayashi and H. Nakano. PX: A Computational Logic. Foundations of Computing. MIT Press, Cambridge, MA, 1988."},{"key":"11_CR18","unstructured":"D. J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"D. J. Howe. Equality in lazy computation systems. Proc. Fourth Symp. Logic in Computer Science, IEEE, 1989.","DOI":"10.1109\/LICS.1989.39174"},{"key":"11_CR20","series-title":"Technical report","volume-title":"Logic programming in the nuprl type theory environment","author":"J. Lipton","year":"1991","unstructured":"J. Lipton. Logic programming in the nuprl type theory environment. Technical report, Cornell University, Ithaca, NY, 1991. To appear as a technical report, summer 1991."},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Z. Luo. Ecc, an extended calculus of construction. In Proc. Fourth Symp. on Logics in Computer Science, IEEE, Washington, DC, June 1989.","DOI":"10.1109\/LICS.1989.39193"},{"key":"11_CR22","first-page":"73","volume-title":"An intuitionistic theory of types: predicative part","author":"P. Martin-Lof","year":"1973","unstructured":"P. Martin-Lof. An intuitionistic theory of types: predicative part. In Logic Colloquium '73., pages 73\u2013118. Amsterdam:North-Holland, 1973."},{"key":"11_CR23","first-page":"153","volume-title":"Constructive mathematics and computer programming","author":"P. Martin-Lof","year":"1982","unstructured":"P. Martin-Lof. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u201375. Amsterdam:North Holland, 1982."},{"key":"11_CR24","unstructured":"P. Mendler. Recursive Types and Type Constraints in Second-Order Lambda Calculus. Proc. in Second Symp. on Logic in Comp. Sci., IEEE, pages 30\u201336, June 1987."},{"key":"11_CR25","volume-title":"Inductive Definition in Type Theory","author":"P. Mendler","year":"1988","unstructured":"P. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1988."},{"key":"11_CR26","unstructured":"C. Murthy. Extracting Constructive Content for Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. TR 89-1151."},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"C. Murthy. An evaluation semantics for classical proofs. In LICS, '91, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151634"},{"key":"11_CR28","series-title":"Technical Report","volume-title":"A constructive proof of higman's lemma","author":"C. Murthy","year":"1989","unstructured":"C. Murthy and J. Russell. A constructive proof of higman's lemma. Technical Report TR 89-1049, Cornell University, Ithaca, NY 14853, January 1989."},{"key":"11_CR29","volume-title":"Programming in Martin-Lof's Type Theory","author":"B. Nordstrom","year":"1990","unstructured":"B. Nordstrom, K. Peterson, and J. Smith. Programming in Martin-Lof's Type Theory. Oxford Sciences Publication, Oxford, 1990."},{"key":"11_CR30","unstructured":"C. Paulin-Mohring. Extraction in the calculus of constructions. PhD thesis, University of Paris VII, 1989."},{"key":"11_CR31","unstructured":"R. Pollack. Lego user's guide. Technical report, University of Edinburgh, 1990."},{"key":"11_CR32","volume-title":"Partial Objects in Type Theory","author":"S. Smith","year":"1989","unstructured":"S. Smith. Partial Objects in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1989."},{"key":"11_CR33","first-page":"183","volume-title":"Symposium on Logic in Computer Science","author":"S. F. Smith","year":"1987","unstructured":"S. F. Smith and R. L. Constable. Partial objects in constructive type theory. In Symposium on Logic in Computer Science., pages 183\u201393. Washington, D.C.:IEEE., 1987."},{"key":"11_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. M. Smullyan","year":"1968","unstructured":"R. M. Smullyan. First-Order Logic. Springer-Verlag, New York, 1968."},{"key":"11_CR35","unstructured":"J. Underwood. A constructive completeness proof for the intuitionistic propositional calculus. Technical report, Cornell University, 1990."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:54:11Z","timestamp":1605646451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}