No.041 NII Shonan School on Coq

Icon

NII Shonan Meeting Seminar 041

Photos

Photos contributed by Ms. Kaori Sugawara (Shonan-village Center)
excursion 2014-08-27 14 13 24 (598x800) excursion 2014-08-27 14 13 47 (1280x956) excursion 2014-08-27 14 55 14 (1024x765) excursion 2014-08-27 18 22 27 (800x598) excursion 2014-08-27 18 22 32 (800x598) excursion 2014-08-27 18 22 40 (800x598) excursion 2014-08-27 18 22 44 (800x598)

Organizers

Lecturers

*2013 ACM Software System Award?Laureate

Sponsors

logos

Overview


Dates: 25 – 29 August 2014
Deadline: Friday, May 2nd, 2014

The objective of this school is to teach the use of the Coq?proof assistant that has received the SIGPLAN Programming Languages Software 2013 Award?and the 2013 ACM Software System Award.?It will consist of lectures and practices in English by internationally renowned experts in Coq.

Prerequisites. No previous knowledge of Coq will be necessary to follow the lectures. Students are however requested to attend the school with their own computer with the latest stable version of Coq and one of its user interfaces (CoqIDE – distributed with Coq, or Proof General) installed. They are freely available online:

What is the Coq?proof assistant? In principle, all mathematics can be formalized in axiomatic set theory, and then checked automatically by a computer. In the last century, more practical foundations for mathematics, based on type theory, have been designed and implemented as proof assistants. One of the most prominent is Coq, developed in France since 1984. They can check proofs and organize them in searchable libraries. They also provide convenient interfaces that help the user make proofs incrementally, and fill in automatically the trivial parts.

What can be done with Coq? In the beginning, proof assistants could only be used to formalize toy examples. It is however not anymore the case. Proof assistants have reached maturity and can deal with difficult mathematical results. For example, in December 2004, Gonthier has announced the full formalization of the four colors theorem in the Coq?proof assistant (cf. Notices of the AMS 55(11), 2008). A more recent example is the proof of the Feit-Thompson theorem completed in Coq in 2012.

Mathematicians are not the only ones to make mathematical proofs. Computer scientists, for instance, make their own proofs. In a software, a small error can indeed result in serious damages in terms of safety and security. It is thus important to provide formal proofs that a software is correct: extensive testing of software or hardware is not enough because it may still miss errors that would be avoided with the use of a proof assistant. One prominent example is the formalization of a complete Java Card system in the Coq?proof assistant and the certification that it meets the highest security requirements for industrial product, i.e., the Common Criteria EAL7 level. This was achieved in 2003 by Trusted Logic, a company that provides secure software for smart cards, terminals and consumer devices. Another example is the compiler Compcert: it is proved in Coq that it will always generate assembly code that has the same semantics than the source code in C. From the mathematician’s eye, some of those proofs may not appear difficult but they are nonetheless tricky and error-prone because they involve huge formal objects such as programs or automata, or require to consider hundreds of cases.

Schedule

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)

09:00~
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

13:30~
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)

08:30~
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

13:30~
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)

08:30~
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

13:00~
excursion, directly followed by the banquet in the evening

August 28th (Thursday)

08:30~
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.

13:30~
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

Protected: Resources

This content is password protected. To view it please enter your password below:

Fee

The participation fee including full board, meeting fees and applicable taxes is 12,500 JPY per day.

  • Participants must share a twin room (two participants per room).
  • Excursion fee, around 5,000 JPY, is not included in the participation fee.
  • We will NOT support travel for any participants.

Participants are expected to attend the full program and excursion staying at Shonan Village Center throughout the all school dates.

How to apply

Application is open to Master students, PhD students, and people from academy or industry who want to use Coq in their work.?We might also consider applications by Bachelor students in exceptional cases.?While the level of the lectures is intended to be accessible to motivated beginners (with some background in logic or mathematics), it should also be interesting to Coq users who wish to deepen their understanding of the system.

Because of limited space, there will be a pre-selection of participants by the organizers. If you wish to participate, please send as soon as possible and no later than?May 2nd, an email explaining in a few words why you wish to participate to?coq-school@math.nagoya-u.ac.jp. In case of students coming from outside of Japan, please also submit a recommendation letter by one of your professors.