ePrints

Semantic Models for a Logic of Partial Functions

Lookup NU author(s): Professor Cliff JonesORCiD, Matthew Lovert

Downloads

• Published version [.pdf]

Abstract

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.

Publication metadata

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

Share