NWI-I00139
Proof Assistants
Course infoSchedule
Course moduleNWI-I00139
Credits (ECTS)6
CategoryMA (Master)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
Lecturer(s)
Coordinator		dr. F. Wiedijk
Other course modules lecturer
Lecturer		dr. F. Wiedijk
Other course modules lecturer
Contactperson for the course		dr. F. Wiedijk
Other course modules lecturer
Academic year2017
Period
KW3-KW4  (05/02/2018 to 02/09/2018)
Starting block
KW3
Course mode
full-time
RemarksThe course is taught in alternating years, and will not be taught in 2017.
Registration using OSIRISNo
Course open to students from other facultiesNo
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims
After the course students can:
  • develop a formalization in a proof assistant
  • implement a simple proof assistant
  • select an appropriate proof assistant for a given purpose
  • install and use a proof assistant that they have not seen before

Content
This course is an introduction to the field of proof assistants, also known as proof checkers or interactive theorem provers. These are implementations of logical systems, programs for the development and verification of formal proofs, both for mathematics and for computer science.  The course presents the current state of the art in proof assistants, and then teaches two specific proof assistants in detail.  
The first of these is the Isabelle system.  With this proof assistant we focus on the user perspective, and will develop a non-trivial proof in full detail.  The second is the HOL system.  With this system we focus on the implementation architecture and automation of the system.  Finally an overview of the main current proof assistants is presented, and some of the large efforts in this area that are currently ongoing are reviewed.
Proof assistants, both for mathematics and for computer science, are one of the research topics of the Intelligent Systems group.
Literature
There are various documents that will be used to support the course. These will be made available on the website in pdf format.

The main of these documents are course notes on the Mizar system by Freek Wiedijk, and the manual of the HOL Light system by John Harrison.

Teaching formats

• 24 hours computer course
• 24 hours lecture
• 16 hours student presentation
• 104 hours individual study period
Extra information teaching methods: The course has three parts:

• Isabelle: using a proof assistant
• HOL: implementing a proof assistant
• overview of the other proof assistants
The first two parts consists of lectures. During these parts students will be working on exercises during the practicum. There will be a final exercise for each of these two parts, that will have to be handed in.

The third part consists of presentations by the students. Each student will present a different proof assistant. As preparation for this part there is one lecture with an overview of proof assistant, to enable students to make a motivated choice for their presentation.

Topics
• the Isabelle proof assistant
• the HOL proof assistant
• the LCF-architecture for proof assistants
• defining and proving in a proof assistant
• advanced type systems for proof assistants
• searching for lemmas in a proof assistant
• proof automation and decision procedures
• goals oriënted proof
• rewriting and more general conversions
• applications of proof assistants

Test information
The final note will be the average of three marks:

• the mark for the Isabelle formalization
• the mark for the small LCF-style proof assistant
• the mark for the presentation in the third part of the course

Prerequisites
Predicate logic. Basic set theory. Lambda calculus.

Required materials
Blackboard
There are various documents that will be used to support the course. These will be made available on the website in pdf format. The main of these documents are course notes on the Mizar system by Freek Wiedijk, and the manual of the HOL Light system

Instructional modes
Course occurrence

Lecture

Practical computer training

Presentation

Zelfstudie

Tests
Tentamen
Test weight1
OpportunitiesBlock KW4, Block KW4