Church's simple theory of types is a system of higher-order logic in which functions are assumed to be total. We present in this paper a version of Church's system called $\mathbf\mathrm{PF}$ in which functions may be partial. The semantics of $\mathbf\mathrm{PF}$, which is based on Henkin's general-models semantics, allows terms to be nondenoting but requires formulas to always denote a standard truth value. We prove that $\mathbf\mathrm{PF}$ is complete with respect to its semantics. The reasoning mechanism in $\mathbf\mathrm{PF}$ for partial functions corresponds closely to mathematical practice, and the formulation of $\mathbf\mathrm{PF}$ adheres tightly to the framework of Church's system.