Skip to main content
SpringerLink
Log in

Curry-Howard Terms for Linear Logic

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to Girard's proof using proof-nets.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Benton, N., G. Bierman, V. de Paiva and M. Hyland, ‘A Term Calculus for Intuitionistic Linear Logic’, p. 75–90 in Typed Larnbda Calculi and Applications, International Conference TLCA '93, Springer Lecture Notes in Computer Science 664, Springer, Berlin (1993).

    Google Scholar 

  2. Crossley, J. N., and J. C. Shepherdson, ‘Extracting programs from proofs by an extension of the Curry-Howard process’, p. 222–288 in Logical Methods, ed. J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler, Birkhäuser, Boston (1993).

    Google Scholar 

  3. Szabo, M. E., The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam (1969).

    Google Scholar 

  4. Girard, J.-Y., Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thése de Doctorat d'État, Université Paris VII (1972).

  5. Girard, J.-Y., ‘Linear logic’, Theoretical Computer Science 50 (1987), 1–102.

    Google Scholar 

  6. Girard, J.-Y., ‘Linear logic: a survey’, preprint Laboratoire de Mathématiques Discrétes.

  7. Girard, J.-Y., A. Scedrov and P. J. Scott, ‘Bounded linear logic: a modular approach to polynomial time computability’, extended abstract in Feasible mathematics, eds. Buss & P. J. Scott, Birkhäuser, Boston, 1990; complete version in TCS 97 (1992), 1–66.

    Google Scholar 

  8. Howard, W. A., ‘The formulae-as-types notion of construction’, p. 479–490 in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J. P. Soldin and J. R. Hindley, Academic Press, London (1980).

    Google Scholar 

  9. Tait, W. W., ‘Intensional interpretation of functionals of finite type I’, Journal of Symbolic Logic 32 (1967), 198–212.

    Google Scholar 

  10. Troelstra, A. S., Lectures on Linear Logic, Stanford, CA: Center for the study of language and information, Nr. 29, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of California, Santa Cruz, CA, USA

    Frank A. Bäuerle

  2. Department of Computer Science, Monash University, Melbourne, Australia

    David Albrecht & John N. Crossley

  3. Department of Mathematics, Monash University, Melbourne, Australia

    John S. Jeavons

Authors
  1. Frank A. Bäuerle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Albrecht
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. John N. Crossley
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. John S. Jeavons
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bäuerle, F.A., Albrecht, D., Crossley, J.N. et al. Curry-Howard Terms for Linear Logic. Studia Logica 61, 223–235 (1998). https://doi.org/10.1023/A:1005025414656

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1005025414656

Search

Navigation