Skip to main content
SpringerLink
Log in

Programs with continuations and linear logic

  • Conference paper
  • First Online:
Book cover Theoretical Aspects of Computer Software (TACS 1991)

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

Included in the following conference series:

  • 139 Accesses

Abstract

A programming language with continuations is studied in the framework of Girard's linear logic. The execution of a program with continuations is in general non-deterministic: the result of computation depends on the evaluation strategy, e.g. call-by-value evaluation, call-by-name evaluation, ..., etc. In this paper, we first introduce λ →c , a programming language with continuations, and then define the translation from λ →c to linear logic, which eliminates the non-determinism of λ →c . The relation between computation of λ →c and normalization of linear logic is also shown.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52:205–237, 1987.

    Article  Google Scholar 

  2. A. Filinski. Declarative continuations and categorical duality. Master's thesis, University of Copenhagen, Aug 1989. DIKU Raport Nr. 89/11, ISSN 0107-8283.

    Google Scholar 

  3. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

    Article  Google Scholar 

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

    Google Scholar 

  5. T. G. Griffin. A formulae-as-types notion of control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1990.

    Google Scholar 

  6. G. Huet. A uniform approach to type theory. Rapports de Recherche, 795, Feb. 1988.

    Google Scholar 

  7. C. Murth and R. L. Constable. Finding computational content in classical proofs, July 1990.

    Google Scholar 

  8. J. Rees and W. Clinger. Revised3 repord on the algorithmic language scheme. SIGPLAN Notices, 21(12):37–79, 1986.

    Google Scholar 

  9. J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Institute for Mathematical Sciences, Kyoto University, 606, Kyoto, JAPAN

    Shin-ya Nishizaki

Authors
  1. Shin-ya Nishizaki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Takayasu Ito Albert R. Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nishizaki, Sy. (1991). Programs with continuations and linear logic. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_62

Download citation

  • DOI: https://doi.org/10.1007/3-540-54415-1_62

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54415-9

  • Online ISBN: 978-3-540-47617-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation