{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:10:34Z","timestamp":1725466234648},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054265","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"270-285","source":"Crossref","is-referenced-by-count":3,"title":["Admissibility of fixpoint induction over partial types"],"prefix":"10.1007","author":[{"given":"Karl","family":"Crary","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"26_CR1","unstructured":"S. Allen. A non-type-theoretic definition of Martin-L\u00f6f's types. In Second IEEE Symposium on Logic in Computer Science, pages 215\u2013221, Ithaca, New York, June 1987."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"P. Audebaud. Partial objects in the calculus of constructions. In Sixth IEEE Symposium on Logic in Computer Science, pages 86\u201395, Amsterdam, July 1991.","DOI":"10.1109\/LICS.1991.151633"},{"key":"26_CR3","volume-title":"The Coq Proof Assistant Reference Manual","author":"B. Barras","year":"1996","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sa\u00cfbi, and B. Werner. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, CNRS and ENS Lyon, 1996."},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"D. A. Basin. An environment for automated reasoning about partial functions. In Ninth International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012825"},{"key":"26_CR5","unstructured":"R. Constable, S. Allen, H. Bromley, W. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, N. Mendler, P. Panangaden, J. Sasaki, and S. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"26_CR6","unstructured":"R. L. Constable and K. Crary. Computational complexity and induction for partial computable functions in type theory. Technical report, Department of Computer Science, Cornell University, 1997."},{"key":"26_CR7","unstructured":"R. L. Constable and S. F. Smith. Partial objects in constructive type theory. In Second IEEE Symposium on Logic in Computer Science, pages 183\u2013193, Ithaca, New York, June 1987."},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"R. L. Constable and S. F. Smith. Computational foundations of basic recursive function theory. In Third IEEE Symposium on Logic in Computer Science, pages 360\u2013371, Edinburgh, Scotland, July 1988.","DOI":"10.1109\/LICS.1988.5133"},{"key":"26_CR9","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 constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"K. Crary. Admissibility of fixpoint induction over partial types. Technical Report TR98-1674, Department of Computer Science, Cornell University, Apr. 1998.","DOI":"10.1007\/BFb0054265"},{"key":"26_CR11","volume-title":"PhD thesis","author":"K. Crary","year":"1998","unstructured":"K. Crary. Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1998. Forthcoming."},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"26_CR13","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0747-7171(92)90026-Z","volume":"14","author":"R. Harper","year":"1992","unstructured":"R. Harper. Constructing type systems over an operational semantics. Journal of Symbolic Computation, 14:71\u201384, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"26_CR14","unstructured":"W. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"D. J. Howe. Equality in lazy computation systems. In Fourth IEEE Symposium on Logic in Computer Science, 1989.","DOI":"10.1109\/LICS.1989.39174"},{"key":"26_CR16","unstructured":"S. Igarashi. Admissibility of fixed-point induction in first-order logic of typed theories. Technical Report AIM-168, Computer Science Department, Stanford University, May 1972."},{"key":"26_CR17","volume-title":"PhD thesis","author":"P. B. Jackson","year":"1995","unstructured":"P. B. Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Jan. 1995."},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"D. MacQueen. Using dependent types to express modular structure. In Thirteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 277\u2013286, St. Petersburg Beach, Florida, Jan. 1986.","DOI":"10.1145\/512644.512670"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress of Logic, Methodology and Philosophy of Science, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153\u2013175. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"issue":"2","key":"26_CR21","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1017\/S0956796800001040","volume":"4","author":"B. C. Pierce","year":"1994","unstructured":"B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207\u2013247, Apr. 1994.","journal-title":"Journal of Functional Programming"},{"key":"26_CR22","unstructured":"D. Scott. Outline of a mathematical theory of computation. In Fourth Princeton Conference on Information Sciences and Systems, pages 169\u2013176, 1970."},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"D. Scott. Lattice theoretic models for various type-free calculi. In Fourth International Congress of Logic, Methodology and Philosophy of Science. North-Holland, 1972.","DOI":"10.1016\/S0049-237X(09)70356-8"},{"key":"26_CR24","volume-title":"PhD thesis","author":"S. F. Smith","year":"1989","unstructured":"S. F. Smith. Partial Objects in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Jan. 1989."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:46:09Z","timestamp":1555656369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0054265","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}