Jan 1, 0400 Comments Off on Schedule
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
