Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id GAA27097 for qed-out; Tue, 13 Jun 1995 06:14:40 -0500
Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id GAA27091 for <qed@mcs.anl.gov>; Tue, 13 Jun 1995 06:14:17 -0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 13 Jun 1995 12:08:29 +0100
X-Uri: <URL:http://www.cl.cam.ac.uk/users/jrh>
To: qed@mcs.anl.gov
Subject: Re: Undefined terms
Date: Tue, 13 Jun 1995 12:08:24 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:286540:950613110840"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


On the subject of ways of dealing with partial functions, I also got the
following message which I've been asked to forward to QED.

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