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; Wed, 3 Mar 1993 20:52:57 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13775;
          Wed, 3 Mar 93 12:28:05 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA13770;
          Wed, 3 Mar 93 12:27:56 -0800
Received: by grolsch.cs.ubc.ca id AA21568 (5.65c/IDA-1.3.5 
          for info-hol@ted.cs.uidaho.edu); Wed, 3 Mar 1993 12:27:29 -0800
Date: 3 Mar 93 12:27 -0800
From: Sreeranga Rajan <sree@ca.ubc.cs>
To: info-hol <info-hol@edu.uidaho.cs.ted>
Cc: peters <peters@edu.uark.mozart>
Message-Id: <981*sree@cs.ubc.ca>
Subject: Re: extracting code

As Paul pointed out, proofs by contradiction in classical logic
pose a major problem for extracting programs.
A good reference on the theoretical aspects is:

	Extracting Constructive Content from Classical Proofs
	(PhD Thesis), by Chet Murthy, Cornell CS Dept, 1990.

In particular, Chet discusses the difficulties due to
axiom of choice and excluded middle of classical logic.

-Sree