# Agathe Chollet

PhD

currently ATER in the LIM at the Reunion University

## Introduction

### CV

You can download my CV as a PDF file .

### Qualifications

- section 25, Mathematics
- section 26, Applied mathematics
- section 27, Computer science

### Thesis

I graduaded in december 2010 : the thesis as a PDF file.

It has been led at the
Laboratoire Mathématiques Images et Application

MIA-MI (Math‑Images) team,
La Rochelle university

My scientific advisors :

- Guy Wallet from MIA (La Rochelle)
- Laurent Fuchs from SIC-Xlim (Poitiers)
- Eric Andres from SIC-Xlim (Poitiers)
- Gaelle Largeteau-Skapin from SIC-Xlim (Poitiers)

My thesis committee :

- Jean Petitot (Primary)
- Gilles Dowek (Member)
- Henry Lombardi (Member)
- Jean-Pierre Reveillès (Member)
- Michel Berthier
- Guy Wallet
- Eric Andres
- Laurent Fuchs

## Research works

**Keywords** : Nonstandard Analysis, Discrete Geometry, Constructive Mathematics

### Summary

We study the transition from the discrete to the continuous world in order to gain understanding of fundamental aspects of discrete geometry. Geometrical objects usually have a natural definition in the continuous world while it is difficult to find discrete analogous notions. Moreover, the computer treatment of these issues justifies the search of a constructive mathematical framework that offers an exact control of computations and an easy implementation.

From this double point of view, there exists an interesting numerical system because it is both discrete and continuous and it seems relatively constructive : this is the so-called Harthong-Reeb line which leads to the deﬁnition of the discrete analytical line by J.P. Reveillès.

Initially, we proposed a rigorous construction of the Harthong-Reeb line using a minimal form of nonstandard analysis. We described a process of arithmetization of continuous functions and we studied the constructive content of this system. Subsequently, we improved the constructive property of this numerical system by substituting the number theory of Laugwitz and Schmieden by usual nonstandard analysis. The new approach of the arithmetization process leads to the introduction of a discrete multi-resolution representation of continuous functions.

Our third step is to transfer these different notions in the Constructive Type Theory of Martin-Lof. The use of this framework, at the boundary between mathematics, logics and computer science, will guarantee a direct implementation in a high level computer language like Coq. An interesting consequence of our work on the Harthong-Reeb line is that this new numerical system appears as a new model of the constructive continuum.

Our programs are developed on a functional language OCaml. In parallel of the theoretical studies of the constructive content of our models, we prove with the formal proof management system Coq the validity of our proofs.

### Ongoing Projects

Formalization and demonstration of our discrete/continuous reals models in Coq avec Nicolas Magaud

### Publications

#### International conferences

- Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective N Magaud, A Chollet, L Fuchs in Automated Deduction in Geometry, 2010, LNCS. PDF
- Omega-arithmetization of elipse. A Chollet, G Wallet, E Andres, L Fuchs, G Largetau-Skapin, A Richard in CompImage, 2010, LNCS. PDF
- Arithmetization with Ω-Integers: A New Multi-resolution
Formalization.
A Chollet, G Wallet, L Fuchs, E Andres, G Largetau-Skapin, Springers’s LNCS
Volume 5852 for IWCIA conference
*(Best-Paper Studient)*. PDF - A ﬁrst look into a formal and constructive approach for discrete geometry using nonstandard analysis. L Fuchs, G Largeteau-Skapin, G Wallet, E Andres, A Chollet, DGCI 2008 (2008) 21–32. PDF

#### International Journals

- Insight in discrete geometry and computational content of a discrete model of the continuum. A Chollet, G Wallet, L Fuchs, G Largeteau-Skapin, E Andres, Pattern recognition , vol 42, num 10 (october 2009). PDF

## Teaching

*Fundamental mathematics*, L1 Math-Phy-Comp, Reunion university*Analysis*, L1 Bio-Chem-Geol, Reunion university*Linear algebra*, L1 Phy-Chem, Reunion university*Computers architecture*, L1 sciences, Reunion university*Matrix calculous*, L1 Math-Comp and Phy-Chem, 2010-2011, Mediterranee university*Geometry and matricial calculous*, L1 MASS, 2010-2011, Mediterranée university*Geomatics*, whole teaching, L2 Geography, 2009-2010 and 2010-2011, La Rochelle university*General mathematics*, L1 Civil engineering, 2009-2010, La Rochelle university