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 year2020
Period
KW3-KW4  (25/01/2021 to 31/08/2021)
Starting block
KW3
Course mode
full-time
Remarks-
Registration using OSIRISYes
Course open to students from other facultiesYes
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.

Instructional Modes
  • Lecture
  • Presentation
  • Self-study
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

    Required materials
    Learning Management System (Brigthspace)
    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

    General
    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.

    Remark
    • 24 hours computer course
    • 24 hours lecture
    • 16 hours student presentation
    • 104 hours individual study peri

    Practical computer training

    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