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)
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