Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Thu, 18 Feb 1993 21:20:01 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA27600;
          Thu, 18 Feb 93 13:04:01 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA27592;
          Thu, 18 Feb 93 13:03:44 -0800
Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0nPIPB-000O0zC;
          Thu, 18 Feb 93 23:03 SAST
Received: by elc.mth.uct.ac.za (4.1/SMI-4.1) id AA12105;
          Thu, 18 Feb 93 23:01:59+020
From: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Message-Id: <9302182101.AA12105@elc.mth.uct.ac.za>
Subject: Re: Completeness proofs
To: annap@edu.uiuc.cs.ganges (Anna Lynn Patterson)
Date: Thu, 18 Feb 93 23:01:58 EET
Cc: info-hol@edu.uidaho.cs.ted (Info-hol mailing list)
In-Reply-To: <8202182049.AA03527@ganges.cs.uiuc.edu>; from "Anna Lynn Patterson" at Feb 18, 82 2:49 pm
X-Mailer: ELM [version 2.3 PL11]

Anna writes:
 
> You know -- I do think someone was trying to use HOL for non-standard
> analysis and wanted to do completeness proofs in HOL.  I am about to
> start embedding a theory and wanted to prove its completeness.  So
> maybe we can discuss it form time to time.  It has to do with
> functional programing language with the addition of state, but with
> keeping higher order functionality -- based on a string of papers by
> Carolyn Talcott and Ian Mason.

How do you plan to set about this? I don't think this is going to
be easy. There is a more general problem here: embedding logics
within HOL, eg programming logics. These all do mostly the same thing,
eg. need propositions of some sort, which are usually modelled as
*predicates* in the HOL logic with the propositional operators
like /\ lifted to the level of predicates.

Maybe it would be useful to set up some generic methods for embedding
logics in HOL. The ideas used in Isabelle may be useful here.

Gavan Tredoux
Faccs lab, Dept Math
UCT