{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T22:45:29Z","timestamp":1774046729186,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540221647","type":"print"},{"value":"9783540248491","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_19","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"293-308","source":"Crossref","is-referenced-by-count":18,"title":["Induction and Co-induction in Sequent Calculus"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Momigliano","sequence":"first","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-44557-9_2","volume-title":"Types for Proofs and Programs","author":"A. Abel","year":"2000","unstructured":"Abel, A., Altenkirch, T.: A predicative strong normalisation proof for a \u03bb-calculus with interleaving inductive types. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 21\u201340. Springer, Heidelberg (2000)"},{"key":"19_CR2","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol.\u00a090, pp. 739\u2013782. North-Holland, Amsterdam (1977)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-45685-6_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Ambler","year":"2002","unstructured":"Ambler, S., Crole, R., Momigliano, A.: Combining higher order abstract syntax with tactical theorem proving and (co)induction. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, p. 13. Springer, Heidelberg (2002)"},{"issue":"2-3","key":"19_CR4","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. Bohm","year":"1985","unstructured":"Bohm, C., Berarducci, A.: Automatic synthesis of typed lambda programs on term algebras. Theoretical Computer Science\u00a039(2-3), 135\u2013153 (1985)","journal-title":"Theoretical Computer Science"},{"key":"19_CR5","unstructured":"Crole, R.L.: Lectures on [Co]Induction and [Co]Algebras. Technical Report 1998\/12, Department of Mathematics and Computer Science, University of Leicester (1998)"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1017\/CBO9780511569807.004","volume-title":"Logical Frameworks","author":"N. de Bruijn","year":"1991","unstructured":"de Bruijn, N.: A plea for weaker frameworks. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 40\u201367. Cambridge University Press, Cambridge (1991)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Despeyroux, J., Hirschowitz, A.: Higher-order abstract syntax with induction in Coq. In: Fifth Conference on Logic Programming and Automated Reasoning, pp. 159\u2013173 (1994)","DOI":"10.1007\/3-540-58216-9_36"},{"key":"19_CR8","unstructured":"Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Nordstr\u00f6m, B., Pettersson, K., Plotkin, G. (eds.) Informal Proceedings Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, June 8\u201312, pp. 193\u2013217, Dept. of Computing Science, Chalmers Univ. of Technology and G\u00f6teborg Univ. (1992)"},{"key":"19_CR9","unstructured":"Gim\u00e9nez, E.: Un Calcul de Constructions Infinies et son Application a la Verification des Systemes Communicants. PhD thesis PhD 96-11, Laboratoire de l\u2019Informatique du Parall \u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon (December 1996)"},{"key":"19_CR10","unstructured":"Girard, J.-Y.: A fixpoint theorem in linear logic. Email to the linear@cs.stanford.edu mailing list (February 1992)"},{"issue":"1","key":"19_CR11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/3-540-48224-5_78","volume-title":"Automata, Languages and Programming","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 963\u2013978. Springer, Heidelberg (2001)"},{"key":"19_CR13","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0049-237X(08)70847-4","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"P. Martin-L\u00f6f","year":"1971","unstructured":"Martin-L\u00f6f, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J. (ed.) Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 179\u2013216. North-Holland, Amsterdam (1971)"},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R. McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science\u00a0232, 91\u2013119 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"19_CR15","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R. McDowell","year":"2002","unstructured":"McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic\u00a03(1), 80\u2013136 (2002)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"3","key":"19_CR16","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/S0304-3975(01)00168-2","volume":"294","author":"R. McDowell","year":"2003","unstructured":"McDowell, R., Miller, D., Palamidessi, C.: Encoding transition systems in sequent calculus. TCS\u00a0294(3), 411\u2013437 (2003)","journal-title":"TCS"},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N.P. Mendler","year":"1991","unstructured":"Mendler, N.P.: Inductive types and type constraints in the second order lambda calculus. Annals of Pure and Applied Logic\u00a051(1), 159\u2013172 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"19_CR18","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments: An extended abstract. In: Proceedings of LICS 2003 (January 2003)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-36576-1_24","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Momigliano","year":"2003","unstructured":"Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher order abstract syntax. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 375\u2013392. Springer, Heidelberg (2003)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","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":"Paulin-Mohring, C.: Inductive definitions in the system Coq: Rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"},{"issue":"2","key":"19_CR21","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1093\/logcom\/7.2.175","volume":"7","author":"L.C. Paulson","year":"1997","unstructured":"Paulson, L.C.: Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation\u00a07(2), 175\u2013204 (1997)","journal-title":"Journal of Logic and Computation"},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Handbook of Automated Reasoning, pp. 1063\u20131147. MIT Press, Cambridge (2001)"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Rohwedder, E., Pfenning, F.: Mode and termination analysis for higher-order logic programs. In: Proc. of the European Symposium on Programming, April 1996, pp. 296\u2013310 (1996)","DOI":"10.1007\/3-540-61055-3_44"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-45931-6_25","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Santocanale","year":"2002","unstructured":"Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 357\u2013371. Springer, Heidelberg (2002)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/BFb0031929","volume-title":"Nonclassical Logics and Information Processing","author":"P. Schroeder-Heister","year":"1992","unstructured":"Schroeder-Heister, P.: Cut-elimination in logics with definitional reflection. In: Pearce, D.J., Wansing, H. (eds.) All-Berlin 1990. LNCS, vol.\u00a0619, pp. 146\u2013171. Springer, Heidelberg (1992)"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-58025-5_65","volume-title":"Extensions of Logic Programming","author":"P. Schroeder-Heister","year":"1994","unstructured":"Schroeder-Heister, P.: Definitional reflection and the completion. In: Dyckhoff, R. (ed.) ELP 1993. LNCS, vol.\u00a0798, pp. 333\u2013347. Springer, Heidelberg (1994)"},{"key":"19_CR27","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1109\/LICS.1993.287585","volume-title":"Eighth Annual Symposium on Logic in Computer Science","author":"P. Schroeder-Heister","year":"1993","unstructured":"Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) Eighth Annual Symposium on Logic in Computer Science, June 1993, pp. 222\u2013232. IEEE Press, Los Alamitos (1993)"},{"key":"19_CR28","unstructured":"Sch\u00fcrmann, C.: Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, CMU-CS-00-146 (2000)"},{"key":"19_CR29","first-page":"420","volume-title":"Proceedings of LICS 1995","author":"A.K. Simpson","year":"1995","unstructured":"Simpson, A.K.: Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS. In: Kozen, D. (ed.) Proceedings of LICS 1995, San Diego, California, June 1995, pp. 420\u2013430. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-36576-1_27","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Spenger","year":"2003","unstructured":"Spenger, C., Dams, M.: On the structure of inductive reasoning: Circular and tree-shaped proofs in the\u03bc-calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 425\u2013440. Springer, Heidelberg (2003)"},{"key":"19_CR31","unstructured":"Tiu, A.: Cut-elimination for a logic with induction and co-induction. Draft, available via (September 2003), \n                    http:\/\/www.cse.psu.edu\/~tiu\/lce.pdf"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T23:12:59Z","timestamp":1676070779000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}