Usability: Formalising (un)definedness in typed lambda calculu


Share/Save/Bookmark

Kuper, J. (1995) Usability: Formalising (un)definedness in typed lambda calculu. In: Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94), 25-30 September 1994, Kazimierz, Poland (pp. pp. 76-90).

[img] PDF
Restricted to UT campus only
: Request a copy
682kB
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.
Item Type:Conference or Workshop Item
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/61923
Official URL:http://dx.doi.org/10.1007/BFb0022248
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page