Usability: Formalising (un)definedness in typed lambda calculi

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

Research output: Contribution to conferencePaperAcademicpeer-review

7 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

Keywords

  • EWI-11087
  • IR-61923

Cite this

Kuper, Jan ; Pacholski, L. (Editor) ; Tiuryn, J. (Editor). / Usability: Formalising (un)definedness in typed lambda calculi. 15 p.
@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",

}

Usability: Formalising (un)definedness in typed lambda calculi. / Kuper, Jan; Pacholski, L. (Editor); Tiuryn, J. (Editor).

1995. 76-90.

Research output: Contribution to conferencePaperAcademicpeer-review

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

ER -