The initial paper on LPF was A Logic Covering Undefinedness in Program Proofs by H. Barringer, J.H. Cheng and C. B. Jones; published in Acta Informatica
The above (and Jen Cheng's thesis) covered the untyped logic; the soundness of the typed version of LPF is tackled in A Typed Logic of Partial Functions Reconstructed Classically by C.B. Jones and C.A. Middelburg; published in Acta Informatica
On the usability of logics which handle partial functions by J. H. Cheng and C. B. Jones; pages 51-69 of 3rd Refinement Workshop, edited by C. Morgan and J. C. P. Woodcock; published by Springer-Verlag, 1991. This is also available as a technical report, UMCS-90-3-1.
A recent useful result is in The Connection between Two Ways of Reasoning about Partial Functions John Fitzgerald and Cliff B. Jones; published in IPL
Partial functions and logics: A warning by C. B. Jones; Information Processing Letters Vol 54, pp 65-67, 1995
Must add (two) with Matthew