Interactive theorem proving

CS-428 / 6 credits

Teacher(s): Barrière Aurèle Aimé Aubin, Pit-Claudel Clément

Language: English

Summary

A hands-on introduction to interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation. Come learn how to write computer-checked proofs and certified bug-free code!

Content

  • Intro to the Coq proof assistant (logic, higher-order functions, tactics)
  • Functional programming (inductive types and fixpoints)
  • Structural induction (data structures and verified algorithms)
  • Interpreter-based program semantics (intro to compiler verification)
  • Inductive relations (predicates, rule induction)
  • Automation and tactics I (bottom-up reasoning and logic programming)
  • Operational program semantics (small-and big-step semantics)
  • Program logics (hoare triples)
  • Automation and tactics II (top-down reasoning)
  • Type systems (Simply-typed lambda calculus)
  • Dependent types and equality proofs
  • Automation and tactics III (proofs by reflection)
  • Real-world theorem proving (various topics)

Learning Prerequisites

Recommended courses

This course assumes no knowledge of programming language theory.  The following courses may be useful, but are not required:

  • CS-320 Computer language processing (to introduce the concept of interpreter)
  • CS-425 Foundations of software (to introduce type systems and the lambda calculus)
  • CS-550 Formal verification (for a different perspective on theorem proving)

Important concepts to start the course

  • Functional programming

Learning Outcomes

  • Implement purely-functional algorithms in the Gallina language
  • Translate informal requirements about software into precise mathematical properties
  • Plan and carry out mechanized proofs in Coq (e.g. maths, algorithms, compilers, type systems)
  • Automate repetitive proof tasks by crafting simple custom decision procedures

Teaching methods

  • Lectures
  • Live-coding sessions

Expected student activities

  • Lectures
  • Programming and verification assignments
  • Project (proposal, check-in, presentation, report)

Assessment methods

  • Take-home programming and verification assignments: 40% of the final grade (3 or 4 labs)
  • Formal verification project: 60% of the final grade (~10 weeks, in teams of 1 to 4 students)

Supervision

Office hours Yes
Assistants No
Forum Yes

Resources

Moodle Link

In the programs

  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional
  • Semester: Spring
  • Exam form: During the semester (summer session)
  • Subject examined: Interactive theorem proving
  • Courses: 2 Hour(s) per week x 14 weeks
  • Exercises: 1 Hour(s) per week x 14 weeks
  • Lab: 2 Hour(s) per week x 14 weeks
  • Type: optional

Reference week

Related courses

Results from graphsearch.epfl.ch.