NII Shonan School on Coq


NII Shonan Meeting Seminar 041


The following program contains seven teaching sessions, each of one being composed?of a 1h30 lecture, then a 1h30 session of exercises on laptops on the same?topic.

As a guiding thread for the lectures, we will formalize the semantics of a toy programming language and prove the equivalence of different semantics.

Note that this tentative program will evolve depending on the interests and the difficulties met by the students.?While this program is designed to ensure that people with?little or no experience using Coq can get on, we intend to adapt it to the?audience so that even experimented people could deepen their understanding?of the system.

August 24th (Sunday)

15:00~19:00 Hotel check-in (early check-in from 12:00 is negotiable)

19:00~21:00 Welcome Banquet

August 25th (Monday)

Morning?Lecture 1: Coq as a functional programming language, by Yves Bertot

  • Introduction to Coq
  • Type checking and computations
  • Functional programming
  • Pattern matching on booleans and natural numbers

Afternoon Lecture 2: Structural recursive programming, by Assia Mahboubi

  • Recursive definitions on natural numbers
  • The list data type
  • Recursive programming on lists
  • Polymorphic types and functions in Coq

August 26th (Tuesday)

Morning Lecture 3:?Propositions and Predicates, by?Assia Mahboubi

  • Representation of logical information through Coq’s type system
  • Propositional, first-order and higher order logic
  • Application to program specifications and mathematical statements

Afternoon Lecture 4:?Interactive Proofs, by?Sandrine Blazy

  • Basic components of interactive theorem proving : statements, goals and tactics
  • Introduction and elimination tactics
  • Proof by induction
  • Rewriting techniques

August 27th (Wednesday)

Morning Lecture 5:??Inductive Predicates I, by Pierre Castéran

  • Inductive predicate definitions
  • Proofs by induction on such a predicate
  • Examples taken from Coq’s standard library

excursion, directly followed by the banquet in the evening

August 28th (Thursday)

Morning Lecture 6:?Representing Programs in Coq, by?Yves Bertot

  • Representation of the abstract syntax and semantics of a toy imperative
    programming language
  • This example uses all the concepts seen in previous lectures.

Afternoon Lecture 7:?Inductive Predicates II, by?Pierre Castéran

  • Continuation of Lecture 5
  • Inversion techniques
  • Comparison between induction on data and induction on predicates
  • Proof of equivalence of small steps and?big steps semantics for our toy language

August 29th (Friday):?Advanced applications and research

08:30~09:30 A Computer-Algebra Based Formal Proof of the Irrationality of ζ(3), by Assia Mahboubi

10:00~11:00 Building a certified optimizing C compiler, by Sandrine Blazy

11:00~12:00 Short presentations by some participants