Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 1996: Computer Science Logic pp 399–413Cite as

A type-free resource-aware λ-calculus

  • Conference paper
  • First Online:

  • 3141 Accesses

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

Abstract

We introduce and study a functional language λr, having two main features. λr has the same computational power of the λ-calculus. λr enjoys the resource-awareness of the typed/typable functional languages which encode the Intuitionistic Linear Logic.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky. Domain theory in logical form. In Proceedings of Symposium on Logic in Computer Science LICS'87, 1987.

    Google Scholar 

  2. S. Abramsky. Computational interpretation of linear logic. Technical Report 90/92, Department of Computing, Imperial College, London, 1990.

    Google Scholar 

  3. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

    Google Scholar 

  4. H.P. Barendregt. The Lambda Calculus. North-Holland, second edition, 1984.

    Google Scholar 

  5. N. Benton, G. Bierman, V. de Paiva, and M. Hyland. Term assignment for intuitionistic linear logic. Technical Report 262, Computer Laboratory, University of Cambridge, August 1990.

    Google Scholar 

  6. P.N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proceedings of Computer Science Logic 1994 (CSL'94), Kazimierz, Poland, volume LNCS 993. Springer-Verlag, September 25–30 1995.

    Google Scholar 

  7. T. Braüner. The Girard translation extended with recursion. BRICS Report Series RS-95-13, BRICS, February 1995.

    Google Scholar 

  8. L. Egidi, F. Honsell, and S. Ronchi della Rocca. Operational, denotational and logical descriptions: a case study. FUNDAMENTA INFORMATICAE, 16(2):149–169, February 1992.

    Google Scholar 

  9. J. Gallier. On the correspondence between proofs and lambda terms. Obtained by ftp, January 1993.

    Google Scholar 

  10. J.-Y. Girard. Geometry of interaction 1: Interpretation of sytem F. In Logic Colloquium'88. North-Holland, 1989.

    Google Scholar 

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

    Google Scholar 

  12. C.A. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. The MIT Press, 1992.

    Google Scholar 

  13. W.A. Howard. To H.B. Curry: Essay on Combinatory Logic, Lambda Calculus and Formalisms, chapter The formulae-as-type notion of construction, pages 479–490. J.R. Hindley and J.P. Seldin editors, Academic press, 1980.

    Google Scholar 

  14. Y. Hyland. A syntactic characterization of the equality in some models of the lambda calculus. Journal of London Mathematical Society, 12(2):83–95, 1976.

    Google Scholar 

  15. G. Kahn. Natural semantics. In Proceedings of Symposium on Theoretical Aspects of Computer Science TACS'87, volume LNCS. Springer-Verlag, 1987.

    Google Scholar 

  16. Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.

    Google Scholar 

  17. P.J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308–320, 1964.

    Google Scholar 

  18. P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In Proceedings of Symposium on Logic in Computer Science LICS'92, pages 235–246, June 1992.

    Google Scholar 

  19. S. Martini and A. Masini. On the fine structure of the exponential rule. In L. Reigner J-Y. Girard, Y. Lafont, editor, Proceedings of the Cornell Linear Logic Workshop, 1993.

    Google Scholar 

  20. G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

    Google Scholar 

  21. G. Plotkin. Structured operational semantics. DAMI report series, Aarhus, 1981.

    Google Scholar 

  22. S. Ronchi della Rocca and L. Roversi. Lambda calculus and intuitionistic linear logic. To appear on STUDIA LOGICA, 199?

    Google Scholar 

  23. L. Roversi. Semantics of λ-calculi designed from Intuitionistic Linear Logic. PhD thesis, Università degli Studi di Pisa, 1995.

    Google Scholar 

  24. L. Roversi. Curry-Howard isomorphism and intuitionistic linear logic. Technical Report 19/96, Università degli Studi di Torino, 1996. Submitted to MSCS.

    Google Scholar 

  25. A.S. Troelstra. Natural deduction for intuitionistic linear logic. Annals of Pure and Applied Logic, 73:79–108.

    Google Scholar 

  26. P. Wadler. A syntax for linear logic. Presented at the Mathematical Foundations of Programming Semantics, New Orleans, April 1993.

    Google Scholar 

  27. C. P. Wadsworth. The relation between computational and denotational properties for Scott's D ∞ model of lambda calculus. SIAM Journal of Computing, 1(5):488–521, 1976.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università degli studi di Torino, C.so Svizzera n.185, 10149, Torino, Italy

    Luca Roversi

  2. Department of Computer Science, Brandeis University, 02254, Waltham, MA, USA

    Luca Roversi

Authors
  1. Luca Roversi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Dirk van Dalen Marc Bezem

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Roversi, L. (1997). A type-free resource-aware λ-calculus. In: van Dalen, D., Bezem, M. (eds) Computer Science Logic. CSL 1996. Lecture Notes in Computer Science, vol 1258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63172-0_52

Download citation

  • DOI: https://doi.org/10.1007/3-540-63172-0_52

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-69201-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation