Semantic Models for a Logic of Partial Functions

  1. Lookup NU author(s)
  2. Professor Cliff Jones
  3. Matthew Lovert
Author(s)Jones CB, Lovert M
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Legacy DateSeptember 2010
Report Number1220
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.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication