Ssreflect Users Discussion List

[Damien Rouhling <>]

Dear all,

It is my great pleasure to invite you to my PhD defence.

It will take place at 1 pm on Monday, September 30, at Inria Sophia Antipolis,
in Morgenstern amphitheatre (Kahn building).

Title:
  Formalisation Tools for Classical Analysis − A Case Study in Control Theory

Abstract:
  In this thesis, we put a library for analysis in the Coq proof assistant to
  the test through a case study in control theory. We formalise a proof of
  stability for the inverted pendulum, a standard example in control
  theory. Controlling the inverted pendulum is challenging because of its
  non-linearity, so that this system is often used as a benchmark for new
  control techniques.

  Through this case study, we identify issues in the tools that are currently
  available for the formalisation of classical analysis and we develop new 
ones
  in order to achieve our formalisation goal. In particular, we try to imitate
  the pen-and-paper proof style thanks to new notations and inference
  mechanisms. This is an essential step to make formal proofs more accessible 
to
  mathematicians.

  We then develop a new library for classical analysis in Coq that integrates
  these new tools and tries to palliate the limitations of the library we
  tested, especially in the domain of asymptotic reasoning. We also experiment
  with this new library on the same formal proof and draw lessons on its
  strengths and weaknesses.

  Finally, we sketch a new methodology in order to address the limitations of
  our library in the particular domain of computation. We exploit a technique
  called refinement to refactor the methodology of proof by reflection, a
  technique that automates proofs through computation and also reduces the 
size
  of proof terms. We implement this methodology on the example of arithmetic
  reasoning in rings and discuss how this work could be used to generalise
  existing tools.

Keywords:
  Formal proof, Coq, classical analysis, control theory, inverted pendulum,
  automation, computation.

The jury will be composed of:
  - Jesús Aransay, Profesor Contratado Doctor, Universida de La Rioja
  - Yves Bertot, Directeur de Recherche, Inria Sophia Antipolis Méditerranée
  - Sylvie Boldo, Directrice de Recherche, Inria Saclay Île de France
  - Cyril Cohen, Chargé de Recherche, Inria Sophia Antipolis Méditerranée
  - Éric Goubault, Professeur, École Polytechnique
  - Étienne Lozes, Professeur, Université de Nice Sophia Antipolis
  - Lawrence Paulson, Professor, University of Cambridge.

Best regards,
Damien Rouhling

Attachment: signature.asc
Description: PGP signature