Semantic Models for a Logic of Partial Functions
 Lookup NU author(s)
 Professor Cliff Jones
 Matthew Lovert




Author(s)   Jones CB, Lovert M 
Publication type   Report 
Series Title   School of Computing Science Technical Report Series 
Year   2010 
Legacy Date   September 2010 
Report Number   1220 
Pages   27 



Full text is available for this publication: 




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. 



Institution   School of Computing Science, University of Newcastle upon Tyne 
Place Published   Newcastle upon Tyne 
Actions   