About Conferences Colloquium Workshops Practical

PATE 2007

Workshop on Proof Assistants and Types in Education

Monday, June 25, 2007, Paris
Part of RDP'07

PATE programme
This workshop is supported by the EU Types Coordination Action.

The purpose of the workshop is to bring together researchers and lecturers interested in applying type theory and proof assistants in teaching.

Contributions are solicited in the following subject areas and related topics:

  • type theory as a language for (teaching) mathematics and programming;
  • computer assisted informal reasoning;
  • tools and languages for teaching math and logic;
  • experience in using proof assistants in class.

Invited Talk

William Farmer, McMaster University: The Use of Formal Reasoning Technology in Mathematics Education: Opportunities and Challenges.

Abstract: Mathematics education is a very attractive market for applications of formal languages and reasoning tools. The number of people who study mathematics in school and university is enormous, and there is strong support for improving mathematics education with the aid of computer technology. There are also excellent opportunities to use formal reasoning technology to enhance, if not transform, how students learn mathematics. For example, proof assistants offer a way to reinvigorate the teaching of proof and deductive reasoning in high school and university. Great as these opportunities may be, they are not easy to pursue. Many challenges stand in their way. Not the least of which is the wide-spread scepticism with which formal reasoning technology is regarded in the mathematics community. This talk will discuss these opportunities and challenges and will argue that bold applications, like an interactive mathematics laboratory based on formal reasoning technology, have the best chance of realizing the opportunities and overcoming the challenges.


Preliminary proceedings will be available at theworkshop.

Organising Committee

webmaster at rdp07 dot org