Skip to main content
SpringerLink
Log in

Dual Calculus with Inductive and Coinductive Types

  • Conference paper
Rewriting Techniques and Applications (RTA 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5595))

Included in the following conference series:

Abstract

This paper gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this paper presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus.

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. Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Information and Computation 125(2), 103–117 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  2. Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Lecture Notes in Mathematics, vol. 897. Springer, Heidelberg (1981)

    Book  MATH  Google Scholar 

  3. Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming, ICFP, pp. 233–243. ACM, New York (2000)

    Google Scholar 

  4. Geuvers, H.: Inductive and Coinductive Types with Iteration and Recursion. In: Proceedings of the 1992 workshop on Types for Proofs and Programs, TYPES, pp. 183–207 (1992)

    Google Scholar 

  5. Kakutani, Y.: Duality between Call-by-Name Recursion and Call-by-Value Iteration. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 506–521. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Kimura, D.: Call-by-Value is Dual to Call-by-Name, Extended. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 415–430. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Kimura, D.: Duality between Call-by-value Reductions and Call-by-name Reductions. IPSJ Journal 48(4), 1721–1757 (2007)

    MathSciNet  Google Scholar 

  8. Mendler, N.P.: Inductive Types and Type Constraints in the Second-Order lambda Calculus. Annals of Pure and Applied Logic 51(1-2), 159–172 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  9. Momigliano, A., Tiu, A.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 293–308. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory. Oxford University Press, Oxford (1990)

    MATH  Google Scholar 

  11. Parigot, M.: Strong normalization for second order classical natural deduction. Journal of Symbolic Logic 62(4), 1461–1479 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  12. Parigot, M.: Strong normalization of second order symmetric lambda-calculus. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 442–453. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. 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 

  14. Selinger, P.: Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Mathematical Structures in Computer Science, pp. 207–260 (2001)

    Google Scholar 

  15. Tatsuta, M.: Realizability interpretation of coinductive definitions and program synthesis with streams. Theoretical Computer Science 122(1–2), 119–136 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  16. Wadler, P.: Call-by-Value is Dual to Call-by-Name. In: Proceedings of International Conference on Functional Programming, ICFP, pp. 189–201 (2003)

    Google Scholar 

  17. Wadler, P.: Call-by-Value is Dual to Call-by-Name – Reloaded. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 185–203. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Tokyo, 7-3-1 Hongo, Tokyo, 113-8656, Japan

    Daisuke Kimura

  2. National Institute of Informatics, 2-1-2 Hitotsubashi, Tokyo, 101-8430, Japan

    Makoto Tatsuta

Authors
  1. Daisuke Kimura
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Makoto Tatsuta
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire PPS, Université Paris Diderot - Paris 7, CNRS, Paris, France

    Ralf Treinen

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kimura, D., Tatsuta, M. (2009). Dual Calculus with Inductive and Coinductive Types. In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02348-4_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02347-7

  • Online ISBN: 978-3-642-02348-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation