{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:54Z","timestamp":1725488634414},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_5","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"55-72","source":"Crossref","is-referenced-by-count":7,"title":["Polytypic Proof Construction"],"prefix":"10.1007","author":[{"given":"Holger","family":"Pfeifer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u03b2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"5_CR1","volume-title":"The Coq Proof Assistant Reference Manual \u2014 Vers. 6.2.4","author":"B. Barras","year":"1998","unstructured":"B. Barras, S. Boutin, and C. Cornes et. al. The Coq Proof Assistant Reference Manual \u2014 Vers. 6.2.4. INRIA, Rocquencourt, 1998."},{"key":"5_CR2","unstructured":"R. Bird and O. de Moor. Algebra of Programming. International Series in Computer Science. Prentice Hall, 1997."},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"C. B\u00f6hm and A. Berarducci. Automatic Synthesis of Typed \u03bb-Programs on Term Algebras. Theoretical Computer Science, 39:135\u2013154, 1985.","journal-title":"Theoretical Computer Science"},{"key":"5_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"Proc. COLOG 88","author":"T. Coquand","year":"1990","unstructured":"T. Coquand and C. Paulin. Inductively Defined Types. In Proc. COLOG 88, volume 417 of LNCS, pages 50\u201366. Springer-Verlag, 1990."},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 4th Int. Conf. on Typed Lambda Calculi and Applications, TLCA\u201999","author":"P. Dybjer","year":"1999","unstructured":"P. Dybjer and A. Setzer. A Finite Axiomatization of Inductive-Recursive Definitions. In J.-Y. Girard, editor, Proc. 4th Int. Conf. on Typed Lambda Calculi and Applications, TLCA\u201999, volume 1581 of LNCS. Springer-Verlag, 1999."},{"key":"5_CR6","unstructured":"M. J. C. Gordon and T. F. Melham (eds.). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","first-page":"240","volume-title":"TAPSOFT\u201989","author":"R. Harper","year":"1989","unstructured":"R. Harper and R. Pollack. Type Checking, Universal Polymorphism, and Type Ambiguity in the Calculus of Constructions. In TAPSOFT\u201989, volume II, LNCS, pages 240\u2013256. Springer-Verlag, 1989."},{"key":"5_CR8","unstructured":"G. Huet and A. Sa\u00efbi. Constructive Category Theory. In Proc. CLICS-TYPES Workshop on Categories and Type Theory, January 1995."},{"key":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-57880-3_20","volume-title":"Programming Languages and Systems \u2014 ESOP\u201994","author":"C.B. Jay","year":"1994","unstructured":"C.B. Jay and J.R.B. Cockett. Shapely Types and Shape Polymorphism. In D. Sannella, editor, Programming Languages and Systems \u2014 ESOP\u201994, volume 788 of LNCS, pages 302\u2013316. Springer-Verlag, 1994."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"J. Jeuring. Polytypic Pattern Matching. In Conf. Functional Programming Languages and Computer Architecture (FPCA\u2019 95), pages 238\u2013248. ACM Press, 1995.","DOI":"10.1145\/224164.224212"},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-61628-4_3","volume-title":"Advanced Functional Programming","author":"J. Jeuring","year":"1996","unstructured":"J. Jeuring and P. Jansson. Polytypic Programming. In T. Launchbury, E. Meijer, and T. Sheard, editors, Advanced Functional Programming, LNCS, pages 68\u2013114. Springer-Verlag, 1996."},{"key":"5_CR12","unstructured":"Z. Luo. An Extended Calculus of Constructions. Technical Report CST-65-90, University of Edinburgh, July 1990."},{"key":"5_CR13","unstructured":"Z. Luo and R. Pollack. The Lego Proof Development System: A User\u2019s Manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992."},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0167-6423(90)90023-7","volume":"14","author":"G. Malcolm","year":"1990","unstructured":"G. Malcolm. Data Structures and Program Transformation. Science of Computer Programming, 14:255\u2013279, 1990.","journal-title":"Science of Computer Programming"},{"issue":"5","key":"5_CR15","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/BF01211391","volume":"4","author":"L. Meertens","year":"1992","unstructured":"L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413\u2013425, 1992.","journal-title":"Formal Aspects of Computing"},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61756-6_73","volume-title":"Programming Languages, Implementations, Logics, and Programs (PLILP\u201996)","author":"L. Meertens","year":"1996","unstructured":"L. Meertens. Calculate Polytypically. In H. Kuchen and S.D. Swierstra, editors, Programming Languages, Implementations, Logics, and Programs (PLILP\u201996), LNCS, pages 1\u201316. Springer-Verlag, 1996."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"E. Meijer, M. Fokkinga, and R. Paterson. Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire. In Proc. 5th Conf. on Functional Programming Languages and Computer Architecture, pages 124\u2013144, 1991.","DOI":"10.1007\/3540543961_7"},{"key":"5_CR18","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J.M. Smith. Programming in Martin-L\u00f6f\u2019s Type Theory. Monographs on Computer Science. Oxford Science Publications, 1990."},{"issue":"Nr. 2","key":"5_CR19","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0890-5401(92)90031-A","volume":"99","author":"Ch.E. Ore","year":"1992","unstructured":"Ch.E. Ore. The Extended Calculus of Constructions (ECC) with Inductive Types. Information and Computation, 99,Nr. 2:231\u2013264, 1992.","journal-title":"Information and Computation"},{"issue":"2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq, Rules and Properties. In J.F. Groote M. Bezem, editor, Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 328\u2013345. Springer-Verlag, 1993."},{"key":"5_CR22","unstructured":"L.C. Paulson. A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definition. Technical report, Computer Laboratory, University of Cambridge, 1996."},{"key":"5_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/3-540-62688-3_44","volume-title":"Proc. 3rd Int. Conf. on Typed Lambda Calculi and Applications TLCA\u201997","author":"H. Rue\u03b2","year":"1997","unstructured":"H. Rue\u03b2. Computational Reflection in the Calculus of Constructions and Its Application to Theorem Proving. In J. R. Hindley P. de Groote, editor, Proc. 3rd Int. Conf. on Typed Lambda Calculi and Applications TLCA\u201997, volume 1210 of LNCS, pages 319\u2013335. Springer-Verlag, 1997."},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"N. Shankar. Steps Towards Mechanizing Program Transformations Using PVS. Preprint submitted to Elsevier Science, 1996.","DOI":"10.1016\/0167-6423(96)00003-2"},{"key":"5_CR25","volume-title":"Type Parametric Programming","author":"T. Sheard","year":"1993","unstructured":"T. Sheard. Type Parametric Programming. Oregon Graduate Institute of Science and Technology, Portland, OR, USA, 1993."},{"key":"5_CR26","unstructured":"The Lego team. The Lego Library. Distributed with Lego System, 1998."},{"key":"5_CR27","unstructured":"D. Tuijnman. A Categorical Approach to Functional Programming. PhD thesis, Universit\u00e4t Ulm, 1996."},{"key":"5_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Mathematical Foundations of Computer Science, Proceedings","author":"F. W. Henke von","year":"1976","unstructured":"F. W. von Henke. An Algebraic Approach to Data Types, Program Verification, and Program Synthesis. In Mathematical Foundations of Computer Science, Proceedings, volume 45 of LNCS. Springer-Verlag, 1976."},{"key":"5_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/BFb0055152","volume-title":"Proc. Intl. Conf. on Theorem Proving in Higher Order Logics","author":"F. W. Henke von","year":"1998","unstructured":"F. W. von Henke, S. Pfab, H. Pfeifer, and H. Rue\u03b2. Case Studies in Meta-Level Theorem Proving. In Jim Grundy and Malcolm Newey, editors, Proc. Intl. Conf. on Theorem Proving in Higher Order Logics, volume 1479 of LNCS, pages 461\u2013478. Springer-Verlag, September 1998."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:58:44Z","timestamp":1556737124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}