John.
| Date: Sun, 4 Jun 95 15:08:16 BST
| From: Cliff B Jones <cliff@cs.man.ac.uk>
| To: John.Harrison@cl.cam.ac.uk
| Cc: pal@everest.cs.uq.oz.au
| In-Reply-To: <9505210127.AA07165@everest> (pal@everest.cs.uq.oz.au)
| Subject: Re: [John.Harrison@cl.cam.ac.uk: Re: Undefined terms]
Sear John Harrison,
Peter Lindsay forwarded your message to QED (I don't receive it).
There is another approach which re-defines the logical operators to
cope with "gaps" (Blamey's phrase). The following paper relate to such
a LPF:
@article{BCJ84,
author = "H. Barringer and J.H. Cheng and C. B. Jones",
title = "A Logic Covering Undefinedness in Program Proofs",
journal = acta,
volume = "21",
pages = "251--269",
year = "1984"
}
@phdthesis{Cheng86,
title = "A Logic for Partial Functions",
author = "J.H. Cheng",
school = "University of Manchester",
year = "1986"
}
@article{JonesMiddelburg94,
author = "C.B. Jones and C.A. Middelburg",
title = "A Typed Logic of Partial Functions Reconstructed
Classically",
journal = "Acta Informatica",
volume = 31,
number = 5,
pages = "399--430",
year = 1994
}
cliff jones