Usability: Formalising (un)definedness in typed lambda calculi

Jan Kuper; L. Pacholski; J. Tiuryn

doi:10.1007/BFb0022248

Usability: Formalising (un)definedness in typed lambda calculi

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

Research output: Contribution to conference › Paper › peer-review

54 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 language	Undefined
Pages	76-90
Number of pages	15
DOIs	https://doi.org/10.1007/BFb0022248
Publication status	Published - 1995
Event	Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94) - Kazimierz, Poland Duration: 25 Sept 1994 → 30 Sept 1994

Conference

Conference	Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94)
Period	25/09/94 → 30/09/94
Other	25-30 September 1994

Keywords

EWI-11087
IR-61923

Access to Document

10.1007/BFb0022248

CSL94

Cite this

@conference{b69b404596034d87bb1210b5873e3229,

title = "Usability: Formalising (un)definedness in typed lambda calculi",

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.",

keywords = "EWI-11087, IR-61923",

author = "Jan Kuper and L. Pacholski and J. Tiuryn",

year = "1995",

doi = "10.1007/BFb0022248",

language = "Undefined",

pages = "76--90",

note = "Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94) ; Conference date: 25-09-1994 Through 30-09-1994",

}

TY - CONF

T1 - Usability: Formalising (un)definedness in typed lambda calculi

AU - Kuper, Jan

A2 - Pacholski, L.

A2 - Tiuryn, J.

PY - 1995

Y1 - 1995

N2 - 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.

AB - 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.

KW - EWI-11087

KW - IR-61923

U2 - 10.1007/BFb0022248

DO - 10.1007/BFb0022248

M3 - Paper

SP - 76

EP - 90

T2 - Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94)

Y2 - 25 September 1994 through 30 September 1994

ER -