乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:42:38Z","timestamp":1725496958115},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418641"},{"type":"electronic","value":"9783540453154"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45315-6_4","type":"book-chapter","created":{"date-parts":[[2007,12,3]],"date-time":"2007-12-03T06:28:39Z","timestamp":1196663319000},"page":"57-71","source":"Crossref","is-referenced-by-count":15,"title":["Type Isomorphisms and Proof Reuse in Dependent Type Theory"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Olivier","family":"Pons","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"4_CR1","unstructured":"J. C. B. Almeida. A formalization of RSA in Coq, July 1999. Available from http:\/\/logica.di.uminho.pt\/CryptoCoq\/index.html ."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"L. Augustsson. Cayenne: A language with dependent types. In Proceedings of ICFP\u201998, pages 239\u2013250. ACM Press, 1998.","DOI":"10.1145\/289423.289451"},{"key":"4_CR3","unstructured":"A. Bailey. The Machine-Checked Literate Formalisation of Algebra in Type Theory. PhD thesis, University of Manchester, 1998."},{"key":"4_CR4","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, H. Laulh\u00e8re, P. Loiseleur, C. Mu\u00f1oz, C. Murthy, C. Parent-Vigouroux, C. Paulin-Mohring, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant User\u2019s Guide. Version 6.3.1, December 1999."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"G. Barthe. Implicit coercions in type systems. In Berardi and Coppo [10], pages 16\u201335.","DOI":"10.1007\/3-540-61780-9_58"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1017\/S0956796899003573","volume":"9","author":"G. Barthe","year":"1999","unstructured":"G. Barthe. Theoretical pearl: type-checking injective pure type systems. Journal of Functional Programming, 9:675\u2013698, 1999.","journal-title":"Journal of Functional Programming"},{"key":"4_CR7","unstructured":"G. Barthe, V. Capretta, and O. Pons. Setoids in type theory. Submitted, 2000."},{"key":"4_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/3-540-49099-X_8","volume-title":"Proceedings of ESOP\u201999","author":"G. Barthe","year":"1999","unstructured":"G. Barthe and M.J. Frade. Constructor subtyping. In D. Swiestra, editor, Proceedings of ESOP\u201999, volume 1576 of Lecture Notes in Computer Science, pages 109\u2013127. Springer-Verlag, 1999."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"G. Barthe, M. Ruys, and H. Barendregt. A two-level approach towards lean proof-checking. In Berardi and Coppo [10], pages 16\u201335.","DOI":"10.1007\/3-540-61780-9_59"},{"key":"4_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of TYPES\u201995","year":"1996","unstructured":"S. Berardi and M. Coppo, editors. Proceedings of TYPES\u201995, volume 1158 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"4_CR11","unstructured":"G. Betarte. Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computer Science, Chalmers Tekniska Hogskola, 1998."},{"key":"4_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/3-540-48685-2_25","volume-title":"Proceedings of RTA\u201999","author":"F. Blanqui","year":"1999","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. The algebraic calculus of constructions. In P. Narendran and M. Rusinowitch, editors, Proceedings of RTA\u201999, volume 1631 of Lecture Notes in Computer Science, pages 301\u2013316. Springer-Verlag, 1999."},{"key":"4_CR13","unstructured":"P. Callaghan and Z. Luo. Plastic: An implementation of typed LF with coercive subtyping and universes. Journal of Automated Reasoning, 200x. To appear."},{"key":"4_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/3-540-48256-3_10","volume-title":"Proceedings of TPHOL\u201999","author":"V. Capretta","year":"1999","unstructured":"V. Capretta. Universal algebra in type theory. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, editors, Proceedings of TPHOL\u201999, volume 1690 of Lecture Notes in Computer Science, pages 131\u2013148. Springer-Verlag, 1999."},{"key":"4_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/3-540-44659-1_5","volume-title":"Proceedings of TPHOLs\u201900","author":"V. Capretta","year":"2000","unstructured":"V. Capretta. Recursive families of inductive types. In M. Aagard and J. Harrison, editors, Proceedings of TPHOLs\u201900, volume 1869 of Lecture Notes in Computer Science, pages 73\u201389. Springer-Verlag, 2000."},{"issue":"1","key":"4_CR16","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/234313.234418","volume":"28","author":"L. Cardelli","year":"1996","unstructured":"L. Cardelli. Type systems. ACM Computing Surveys, 28(1):263\u2013264, March 1996.","journal-title":"ACM Computing Surveys"},{"issue":"4","key":"4_CR17","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17(4):471\u2013522, December 1985.","journal-title":"ACM Computing Surveys"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"P. Cohn. Universal algebra, volume 6 of Mathematics and its Applications. D. Reidel, 1981.","DOI":"10.1007\/978-94-009-8399-1"},{"key":"4_CR19","unstructured":"T. Coquand. Metamathematical investigations of a calculus of constructions. In P. Odifreddi, editor, Logic and Computer Science, pages 91\u2013122. Academic Press, 1990."},{"key":"4_CR20","unstructured":"R. Curien. Outils pour la preuve par analogie. PhD thesis, Universit\u00e9 de Nancy, 1995."},{"key":"4_CR21","unstructured":"D. Delahaye, R. di Cosmo, and B. Werner. Recherche dans une biblioth\u00e8que de preuves Coq en utilisant le type et modulo isomorphismes. In Proceedings of the PRC\/GDR de programmation, P\u00f4le Preuves et Sp\u00e9cifications Alg\u00e9briques, November 1997."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo. Isomorphisms of types: from \u03bb-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995.","DOI":"10.1007\/978-1-4612-2572-0"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Howe. Generalization and reuse of tactic proofs. In F. Pfenning, editor, Proceedings of LPAR\u201994, volume 822 of Lecture Notes in Artificial Intelligence, pages 1\u201315. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58216-9_25"},{"key":"4_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-60579-7_2","volume-title":"Proceedings of TYPES\u201994","author":"H. Geuvers","year":"1995","unstructured":"H. Geuvers. A short and flexible proof of strong normalisation for the Calculus of Constructions. In P. Dybjer, B. Nordstrom, and J. Smith, editors, Proceedings of TYPES\u201994, volume 996 of Lecture Notes in Computer Science, pages 14\u201338. Springer-Verlag, 1995."},{"key":"4_CR25","unstructured":"R. W. Hasker and U. S. Reddy. Generalization at higher types. In D. Miller, editor, Proceedings of the Workshop on the \u03bbProlog Programming Language, pages 257\u2013271. University of Pennsylvania, July 1992. Available as Technical Report MS-CIS-92-86."},{"issue":"1-2","key":"4_CR26","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: Introduction and survey. Theoretical Computer Science, 121(1-2):279\u2013308, 1993.","journal-title":"Theoretical Computer Science"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"T. Kolbe and C. Walther. Proof analysis, generalization, and reuse. In W. Bibel and P. H. Schmidt, editors, Automated Deduction: A Basis for Applications. Volume II, Systems and Implementation Techniques. Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0435-9_8"},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9:105\u2013130, February 1999.","journal-title":"Journal of Logic and Computation"},{"key":"4_CR29","unstructured":"Z. Luo and R. Pollack. LEGO proof development system: User\u2019s manual. Technical Report ECS-LFCS-92-211, LFCS, University of Edinburgh, May 1992."},{"key":"4_CR30","unstructured":"N. Magaud and Y. Bertot. Changements de repr\u00e9sentation des structures de donn\u00e9es dans Coq: le cas des entiers naturels. In P. Casteran, editor, Proceedings of JFLA\u201901, 2001."},{"key":"4_CR31","unstructured":"R. Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994."},{"key":"4_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/3-540-44659-1_29","volume-title":"Proceedings of TPHOLs\u201900","author":"R. Pollack","year":"2000","unstructured":"R. Pollack. Dependently typed records for representing mathematical structures. In M. Aagard and J. Harrison, editors, Proceedings of TPHOLs\u201900, volume 1869 of Lecture Notes in Computer Science, pages 462\u2013479. Springer-Verlag, 2000."},{"key":"4_CR33","unstructured":"O. Pons. Conception et r\u00e9alisation d\u2019outils d\u2019aide au d\u00e9veloppement de grosses th\u00e9ories dans les syst\u00e8mes de preuves interactifs. PhD thesis, Conservatoire National des Arts et M\u00e9tiers, 1999."},{"issue":"1","key":"4_CR34","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S095679680000006X","volume":"1","author":"M. Rittri","year":"1991","unstructured":"M. Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71\u201389, 1991.","journal-title":"Journal of Functional Programming"},{"key":"4_CR35","unstructured":"E. J. Rollins and J. M. Wing. Specifications as search keys for software libraries. In K. Furukawa, editor, Proceedings of ICLP\u201991, pages 173\u2013187. MIT Press, June 1991."},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"A. Saibi. Typing algorithm in type theory with inheritance. In Proceedings of POPL\u201997, pages 292\u2013301. ACM Press, 1997.","DOI":"10.1145\/263699.263742"},{"issue":"1","key":"4_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2708","volume":"143","author":"P. Severi","year":"1998","unstructured":"P. Severi. Type inference for pure type systems. Information and Computation, 143(1):1\u201323, May 1998.","journal-title":"Information and Computation"},{"key":"4_CR38","unstructured":"N. Shankar, S. Owre, and J.M. Rushby. The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, February 1993. Supplemented with the PVS2 Quick Reference Manual, 1997."},{"key":"4_CR39","unstructured":"B. Werner. M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7, 1994."},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of POPL\u201999, pages 214\u2013227. ACM Press, 1999.","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45315-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T13:10:08Z","timestamp":1557061808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45315-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418641","9783540453154"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-45315-6_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}