Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 4 Apr 1994 17:09:24 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA15185; Mon, 4 Apr 1994 09:46:38 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA15179; Mon, 4 Apr 1994 09:46:28 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA10079; Mon, 4 Apr 1994 08:47:25 -0700 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 4 Apr 1994 16:46:44 +0100 To: Sebastian Maneth Cc: info-hol@cs.uidaho.edu Subject: Re: FP synthesis from PC proofs In-Reply-To: Your message of Sat, 26 Mar 94 12:10:06 -0500. <199403261710.AA18401@cygnus.cis.umassd.edu> Date: Mon, 04 Apr 94 16:46:40 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:065410:940404154647"@cl.cam.ac.uk> > My question is, what literature/documentation/programs are available on > program synthesis from logic proofs??? The books "Logical Frameworks" and "Logical Environemnts", edited by G. Huet and G. Plotkin (Cambridge University Press) contain much relevant research. See also "Logic and Computer Science", edited by P. Odifreddi (Academic Press). Lawrence C Paulson, University Lecturer Computer Laboratory, University of Cambridge, Pembroke Street, Cambridge CB2 3QG, England Tel: +44(0)223 334623 Fax: +44(0)223 334678