Usability: Formalising (un)definedness in typed lambda calculi

Jan Kuper, L. Pacholski (Editor), J. Tiuryn (Editor)

    Research output: Contribution to conferencePaperpeer-review

    14 Downloads (Pure)

    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.
    Original languageUndefined
    Pages76-90
    Number of pages15
    DOIs
    Publication statusPublished - 1995
    EventSelected Papers from the 8th International Workshop on Computer Science Logic (CSL'94) - Kazimierz, Poland
    Duration: 25 Sep 199430 Sep 1994

    Conference

    ConferenceSelected Papers from the 8th International Workshop on Computer Science Logic (CSL'94)
    Period25/09/9430/09/94
    Other25-30 September 1994

    Keywords

    • EWI-11087
    • IR-61923

    Cite this