Skip to main content
SpringerLink
Log in

Usability: formalising (un)definedness in typed lambda calculus

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1994)

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

Included in the following conference series:

  • 150 Accesses

Abstract

In this paper we discuss usability, and propose to take that notion as a formalisation of (un)definedness in typed lambda calculus, especially in calculi based on PCF. We discuss some important properties that make usability attractive as a formalisation of (un)definedness. There is a remarkable difference between usability and solvability: in the untyped lambda calculus the solvable terms are precisely the terms with a head normal form, whereas in typed lambda calculus the usable terms are “between” the terms with a normal form and the terms with a (weak) head normal form.

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

  • Abramsky, S. (1990), The Lazy Lambda Calculus, in: Turner, D.A. (Editor), Research Topics in Functional Programming Languages, Addison-Wesley, Reading, Massachusetts.

    Google Scholar 

  • Barendregt, H.P. (1971), Some extensional term models for combinatory logics and lambda calculi, Ph.D. Thesis, Utrecht.

    Google Scholar 

  • Barendregt, H.P. (1975), Solvability in lambda calculi, Colloque International de Logique, Clermont Ferrand, 209–219.

    Google Scholar 

  • Barendregt, H.P. (1984), The Lambda Calculus — Its Syntax and Semantics (revised edition), North-Holland, Amsterdam.

    Google Scholar 

  • Berry, G., P.-L. Curien, J.-J. Lévy (1985), Full abstraction for sequential languages: state of the art, in: Nivat, M. and J.C. Reynolds (Editors), Algebraic Methods in Semantics, Cambridge University Press, Cambridge, 89–132.

    Google Scholar 

  • Kuper, J. (1994), Partiality in Logic and Computation — Aspects of Undefinedness, Ph.D.Thesis, Enschede.

    Google Scholar 

  • Ong, C.-H.L. (1988), The Lazy Lambda Calculus: an Investigation into the Foundations of Functional Programming, Ph.D. Thesis, Imperial College, London.

    Google Scholar 

  • Plotkin, G.D.(1977), LCF considered as a programming language, Theoretical Computer Science 5, 223–255.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Twente, P.O.Box 217, 7500, AE Enschede, The Netherlands

    Jan Kuper

Authors
  1. Jan Kuper
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Leszek Pacholski Jerzy Tiuryn

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kuper, J. (1995). Usability: formalising (un)definedness in typed lambda calculus. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022248

Download citation

  • DOI: https://doi.org/10.1007/BFb0022248

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60017-6

  • Online ISBN: 978-3-540-49404-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation