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
Examiner		dr. F. Wiedijk
Other course modules lecturer
Academic year2019
Period
KW3-KW4  (03/02/2020 to 30/08/2020)
Starting block
KW3
Course mode
full-time
Remarks-
Registration using OSIRISYes
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.
Level

Presumed foreknowledge
Predicate logic. Basic set theory. Lambda calculus.
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
    • Specifics

    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
    Formalisation
    Test weight1
    Test typeAssignment
    OpportunitiesBlock KW4, Block KW4

    Programming assignment
    Test weight1
    Test typeAssignment
    OpportunitiesBlock KW4, Block KW4

    Presentation
    Test weight1
    Test typePresentation
    OpportunitiesBlock KW4, Block KW4