|AboutConferences Colloquium Workshops Practical||
Workshop on Proof Assistants and Types in Education
Part of RDP'07
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:
Invited TalkWilliam 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.
PublicationPreliminary proceedings will be available at theworkshop.
webmaster at rdp07 dot org