Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Mon, 5 Jun 1995 19:34:05 +0100
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) 
          id NAA29638 for qed-out; Mon, 5 Jun 1995 13:19:14 -0500
Received: from scapa.cs.ualberta.ca (root@scapa.cs.ualberta.ca [129.128.4.44]) 
          by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP id NAA29629 
          for <qed@mcs.anl.gov>; Mon, 5 Jun 1995 13:19:04 -0500
Received: from sedalia.cs.ualberta.ca by scapa.cs.ualberta.ca id <13059-3>;
          Mon, 5 Jun 1995 12:18:45 -0600
Subject: To type or not to type
From: Piotr Rudnicki <piotr@cs.ualberta.ca>
To: qed@mcs.anl.gov
Date: Mon, 5 Jun 1995 12:18:37 -0600 (MDT)
X-Mailer: ELM [version 2.4 PL24]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 648
Message-Id: <95Jun5.121845-0600_mdt.13059-3+78@scapa.cs.ualberta.ca>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Hi:

I would like to propose the subject of typing as a topic for discussion during
the QED workshop in Warsaw.  In August, last year there was some discussion
on this forum that started with L. Lamport's note "Types considered
harmful".  I am interested in discussing the following:

0. What do we mean by "type"?

1. How types are handled in various QED-like systems?  
   Here I would like to hear from other people.

1. What are advantages/disadvantages of using types in known proof-checking
   or theorem proving systems?  Users' view vs implementers' view.

2. Why is type theory neglected in mathematical pratice?


Piotr (Peter) Rudnicki