Workshop on History of Logics, Types and Rewriting

Heriot-Watt University, Edinburgh

Tuesday 5 December 2000

Logic provides an essential foundation for any kind of rigorous reasoning in Mathematics and Computer Science, e.g., proving the correctness and safety of computer programs. Different logics have different properties and there is an ongoing search for better logics. Type theories support increasing the expressiveness of programming languages and logics without losing important theoretical properties. Thus, type theories are the foundation of safe (paradox-free) logics and safe programming languages. Rewriting is a method for applying the rules of logic, mathematics, or computation in a stepwise manner. This supports reasoning about efficient computation strategies and equivalences between propositions or programs. Logics, Types and Rewriting have been basic to the design and implementation of programming languages, the formalization of mathematics, and theorem proving. Logics existed for thousands of years. It can also be argued that rewriting and types existed for that long. However, explicit theories of types and rewriting did not exist before the begin of the 20th century. This workshop attempts to assess some historical points and research trends on logics, types and rewriting during the 20th century.

Here is the program of the workshop.

We compiled a list of participants of the workshop. If some of the details need up-dating please let us know.

Here are some photos from the workshop.

Here is information on how to get to Edinburgh, Heriot-Watt, your accommodation, and the workshop.

Speakers and Topics


There is no registration fee.


Questions should be sent to one of: or or

Carsten Butz, Fairouz Kamareddine ( ), and Joe Wells, URL:
Last modified: December 2000.