Skip to main content
SpringerLink
Log in

Induction and Co-induction in Sequent Calculus

  • Conference paper
Types for Proofs and Programs (TYPES 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3085))

Included in the following conference series:

Abstract

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles are based on a proof theoretic notion of definition, following on work by Schroeder-Heister, Girard, and McDowell and Miller. Definitions are essentially stratified logic programs. The left and right rules for defined atoms treat the definitions as defining fixed points. The use of definitions also makes it possible to reason intensionally about syntax, in particular enforcing free equality via unification. The full system thus allows inductive and co-inductive proofs involving higher-order abstract syntax. We extend earlier work by allowing induction and co-induction on general definitions and show that cut-elimination holds for this extension. We present some examples involving lists and simulation in the lazy λ-calculus. Two prototype implementations are available: one via the Hybrid system implemented on top of Isabelle/HOL and the other in the BLinc system implemented on top of λProlog.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abel, A., Altenkirch, T.: A predicative strong normalisation proof for a λ-calculus with interleaving inductive types. In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 21–40. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 90, pp. 739–782. North-Holland, Amsterdam (1977)

    Chapter  Google Scholar 

  3. Ambler, S., Crole, R., Momigliano, A.: Combining higher order abstract syntax with tactical theorem proving and (co)induction. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, p. 13. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Bohm, C., Berarducci, A.: Automatic synthesis of typed lambda programs on term algebras. Theoretical Computer Science 39(2-3), 135–153 (1985)

    Article  MathSciNet  Google Scholar 

  5. Crole, R.L.: Lectures on [Co]Induction and [Co]Algebras. Technical Report 1998/12, Department of Mathematics and Computer Science, University of Leicester (1998)

    Google Scholar 

  6. de Bruijn, N.: A plea for weaker frameworks. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 40–67. Cambridge University Press, Cambridge (1991)

    Chapter  Google Scholar 

  7. Despeyroux, J., Hirschowitz, A.: Higher-order abstract syntax with induction in Coq. In: Fifth Conference on Logic Programming and Automated Reasoning, pp. 159–173 (1994)

    Google Scholar 

  8. Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Nordström, B., Pettersson, K., Plotkin, G. (eds.) Informal Proceedings Workshop on Types for Proofs and Programs, Båstad, Sweden, June 8–12, pp. 193–217, Dept. of Computing Science, Chalmers Univ. of Technology and Göteborg Univ. (1992)

    Google Scholar 

  9. Giménez, E.: Un Calcul de Constructions Infinies et son Application a la Verification des Systemes Communicants. PhD thesis PhD 96-11, Laboratoire de l’Informatique du Parall élisme, Ecole Normale Supérieure de Lyon (December 1996)

    Google Scholar 

  10. Girard, J.-Y.: A fixpoint theorem in linear logic. Email to the linear@cs.stanford.edu mailing list (February 1992)

    Google Scholar 

  11. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  12. 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. 2076, pp. 963–978. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Martin-Löf, 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. 63, pp. 179–216. North-Holland, Amsterdam (1971)

    Chapter  Google Scholar 

  14. McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science 232, 91–119 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic 3(1), 80–136 (2002)

    Article  MathSciNet  Google Scholar 

  16. McDowell, R., Miller, D., Palamidessi, C.: Encoding transition systems in sequent calculus. TCS 294(3), 411–437 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  17. Mendler, N.P.: Inductive types and type constraints in the second order lambda calculus. Annals of Pure and Applied Logic 51(1), 159–172 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  18. Miller, D., Tiu, A.: A proof theory for generic judgments: An extended abstract. In: Proceedings of LICS 2003 (January 2003)

    Google Scholar 

  19. Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher order abstract syntax. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 375–392. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Paulin-Mohring, C.: Inductive definitions in the system Coq: Rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  21. Paulson, L.C.: Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation 7(2), 175–204 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  22. Pfenning, F.: Logical frameworks. In: Handbook of Automated Reasoning, pp. 1063–1147. MIT Press, Cambridge (2001)

    Chapter  Google Scholar 

  23. 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–310 (1996)

    Google Scholar 

  24. Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 357–371. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Schroeder-Heister, P.: Cut-elimination in logics with definitional reflection. In: Pearce, D.J., Wansing, H. (eds.) All-Berlin 1990. LNCS, vol. 619, pp. 146–171. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  26. Schroeder-Heister, P.: Definitional reflection and the completion. In: Dyckhoff, R. (ed.) ELP 1993. LNCS, vol. 798, pp. 333–347. Springer, Heidelberg (1994)

    Google Scholar 

  27. Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) Eighth Annual Symposium on Logic in Computer Science, June 1993, pp. 222–232. IEEE Press, Los Alamitos (1993)

    Chapter  Google Scholar 

  28. Schürmann, C.: Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, CMU-CS-00-146 (2000)

    Google Scholar 

  29. 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–430. IEEE Computer Society Press, Los Alamitos (1995)

    Google Scholar 

  30. Spenger, C., Dams, M.: On the structure of inductive reasoning: Circular and tree-shaped proofs in theμ-calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 425–440. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  31. Tiu, A.: Cut-elimination for a logic with induction and co-induction. Draft, available via (September 2003), http://www.cse.psu.edu/~tiu/lce.pdf

Download references

Author information

Authors and Affiliations

  1. LFCS, University of Edinburgh,  

    Alberto Momigliano

  2. DSI, University of Milan,  

    Alberto Momigliano

  3. LIX, École polytechnique,  

    Alwen Tiu

  4. Computer Science and Engineering Department, Penn State University,  

    Alwen Tiu

Authors
  1. Alberto Momigliano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alwen Tiu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Stefano Berardi

  2. Dipartimento di Informatica, Università di Torino,  

    Mario Coppo

  3. Dipartimento di Informatica, Università di Torino, Corso Svizzera, 185, I-10149, Torino, Italy

    Ferruccio Damiani

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Momigliano, A., Tiu, A. (2004). Induction and Co-induction in Sequent Calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds) Types for Proofs and Programs. TYPES 2003. Lecture Notes in Computer Science, vol 3085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24849-1_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24849-1_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22164-7

  • Online ISBN: 978-3-540-24849-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation