Skip to main content
SpringerLink
Log in

A confluence result for a typed λ-calculus of exception handling with fixed-point

  • Conference paper
  • First Online:
Fundamentals of Computation Theory (FCT 1999)

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

Included in the following conference series:

  • 379 Accesses

Abstract

We prove the confluence of a λ-calculus of exception handling whose typing system and evaluation rules are initially based on classical logic through the Curry-Howard isomorphism and to which we have added a general fixed-point operator.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. H.P. Barendregt. The Lambda Calculus. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984.

    Google Scholar 

  2. R.V. Book and F. Otto. String-rewriting systems. Texts and Monographs in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  3. Ph. de Groote. A simple calculus of exception handling. Lectures Notes in Computer Science, 902:201–215, 1995.

    Google Scholar 

  4. K. Fujita. Calculus of classical proofs 1. Lectures Notes in Computer Science, 1345:321–335, 1997.

    Google Scholar 

  5. J.H. Gallier. On the correspondence between proofs and λ-terms. Cahiers du Centre de Logique (Universitè Catholique de Louvain), 8:55–138, 1995.

    MathSciNet  Google Scholar 

  6. J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Computer Science. Cambridge University Press, 1989.

    Google Scholar 

  7. J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theorical Computer Science, 121:279–308, 1993.

    Article  MATH  Google Scholar 

  8. D. Prawitz. Natural deduction: a proof-theoretical study. Almquist and Wiksell, Stockholm, 1965

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA, Campus Scientifique - B.P. 239, 54506, Vandœuvre-lès-Nancy Cedex, France

    Catherine Pilière

Authors
  1. Catherine Pilière
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Computer Science, “A.I.Cuza” University, 6600, Iaşi, Romania

    Gabriel Ciobanu

  2. Institute of Mathematics of the Romanian Academy, P.O. Box 1-764, 70700, Bucharest, Romania

    Gheorghe Păun

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pilière, C. (1999). A confluence result for a typed λ-calculus of exception handling with fixed-point. In: Ciobanu, G., Păun, G. (eds) Fundamentals of Computation Theory. FCT 1999. Lecture Notes in Computer Science, vol 1684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48321-7_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-48321-7_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66412-3

  • Online ISBN: 978-3-540-48321-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation