Definedness

Questions of definedness are ubiquitous in mathematics. Informally, these involve reasoning about expressions which may or may not have a value. This paper surveys work on logics in which such reasoning can be carried out directly, especially in computational contexts. It begins with a general logic of partial terms, continues with partial combinatory and lambda calculi, and concludes with an expressively rich theory of partial functions and polymorphic types, where termination of functional programs can be established in a natural way.Lecture for mini-conference on Partial Functions and Programming: Foundational Questions, U.C. Irvine, 17 February 1995. I wish to thank Professor Karel Lambert for his work in organizing this conference. (Research supported by grants from the N.S.F.)