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