Browse by author
Lookup NU author(s): Emeritus Professor Cliff JonesORCiD, Matthew Lovert
The Logic of Partial Functions (LPF) is used to reason about propositions that include terms that can fail to denote values. This paper provides semantics for LPF. A Structural Operational Semantics (SOS) provides an intuitive introduction; this is followed by a denotational semantics where the space of denotations is relations which provide an intuitive model of undefined terms. Finally, we illustrate how the denotational semantics can be used as a basis for proofs about propositions that include terms that can fail to denote.
Author(s): Jones CB, Lovert M
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2010
Pages: 27
Print publication date: 01/09/2010
Source Publication Date: September 2010
Report Number: 1220
Institution: School of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
