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 |
| 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 | |  |
