Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 26 Mar 1994 17:28:36 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA06531;
          Sat, 26 Mar 1994 10:10:46 -0700
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 AA06527;
          Sat, 26 Mar 1994 10:10:31 -0700
Received: from cygnus.cis.umassd.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA05952;
          Sat, 26 Mar 1994 09:09:54 -0800
Received: by cygnus.cis.umassd.edu id AA18401 (5.65c/IDA-1.4.4 
          for info-hol@cs.uidaho.edu); Sat, 26 Mar 1994 12:10:09 -0500
From: Sebastian Maneth <semaneth@cis.umassd.edu>
Message-Id: <199403261710.AA18401@cygnus.cis.umassd.edu>
Subject: FP synthesis from PC proofs
To: info-hol@cs.uidaho.edu
Date: Sat, 26 Mar 94 12:10:06 EST
X-Mailer: ELM [version 2.3 PL11]

Hi all,

We have just started working on a program synthesis project, which will
ultimately transform a small subset of predicate calculus proofs into
ML programs. After some work on basic proof theory, we are finally 'ready'
to start some programming. (or at least think about the implementation)

Some weeks ago I found out about HOL, and just got HOL90 running on our
system here. It feels to me, that it provides a lot of useful tools for this
kind of task.

My question is, what literature/documentation/programs are available on 
program synthesis from logic proofs???

In Paulson:"ML for the Working Programmer", I read something about extracting
recursive function from inductive proofs. (a book by Constable on Nuprl, is
mentioned in that context) Who has worked with this, or has some kind of 
information. Maybe from similar projects in this field. 


thanks a lot.

Sebastian Maneth
semaneth@cis.umassd.edu