publications.bib
@PHDTHESIS{Magaud03b,
AUTHOR = {Nicolas Magaud},
TITLE = {{C}hangements de {R}eprésentation des {D}onnées dans le {C}alcul des {C}onstructions},
SCHOOL = {{U}niversité de Nice Sophia-Antipolis},
YEAR = 2003,
MONTH = OCT,
ABSTRACT = {{
Nous étudions comment faciliter la réutilisation des
preuves formelles en théorie des types. Nous traitons cette question
lors de l'étude
de la correction du programme de calcul de la racine carrée de GMP.
A partir d'une description formelle, nous construisons
un programme impératif avec l'outil Correctness. Cette description
prend en compte tous les détails de l'implantation, y compris
l'arithmétique de pointeurs utilisée et la gestion de la mémoire. \\
Nous étudions aussi comment réutiliser des preuves formelles lorsque
l'on change la représentation concrète des données.
Nous proposons un outil qui permet d'abstraire
les propriétés calculatoires associées à un type inductif dans
les termes de preuve.
Nous proposons également des outils pour simuler ces propriétés
dans un type isomorphe. Nous pouvons ainsi passer, systématiquement,
d'une représentation des données à une autre dans un développement
formel. }},
URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/these-nmagaud.ps.gz}
}
@ARTICLE{BeMaZi02,
AUTHOR = {Yves Bertot and Nicolas Magaud and Paul Zimmermann},
TITLE = {{A} {P}roof of {GMP} {S}quare {R}oot},
JOURNAL = {Journal of Automated Reasoning},
PUBLISHER = {Kluwer Academic Publishers},
VOLUME = 29,
NUMBER = {3-4},
PAGES = {225--252},
YEAR = 2002,
NOTE = {Special Issue on Automating and Mechanising Mathematics: In honour of N.G. de Bruijn.
An earlier version is available as a research report \cite{RR4475}},
ABSTRACT = {{We present a formal proof (at the implementation level) of an efficient
algorithm proposed by Paul Zimmermann to compute square
roots of arbitrarily large integers.
This program, which is part of the GNU Multiple Precision
Arithmetic Library (GMP), is completely proven within the
Coq system. Proofs are developed using the {\sc Correctness} tool
to deal with imperative features of the program.
The formalization is rather large (more than 13000 lines) and requires
some advanced techniques for proof management and reuse.
}}
}
@INPROCEEDINGS{Magaud03a,
AUTHOR = {Nicolas Magaud},
TITLE = {{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem},
BOOKTITLE = {TPHOLs'2003},
PUBLISHER = {LNCS, Springer-Verlag},
VOLUME = {2758},
YEAR = {2003},
NOTE = {© Springer-Verlag},
ABSTRACT = {
{In a theorem prover like \textsf{Coq}, mathematical concepts can be implemented in several ways.
Their different representations can be either efficient for computing or well-suited
to carry out proofs easily. In this paper, we present improved techniques to
deal with changes of data representation within \textsf{Coq}. We propose a smart handling
of case analysis and definitions together with some general methods to transfer
recursion operators and their reduction rules from one setting to another. Once
we have built a formal correspondence between two settings, we can translate
automatically properties obtained in the initial
setting into new properties in the target setting. We successfully experiment with
changing Peano's numbers
into binary numbers for the whole \textsl{Arith} library of \textsf{Coq} as well as with
changing polymorphic lists into reversed (snoc) lists. }},
PSFILE = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/tphols2003-nmagaud.ps},
URL = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=87}
}
@INPROCEEDINGS{MagaudBertot00,
AUTHOR = {N. Magaud and Y. Bertot},
TITLE = {{Changing data structures in type theory:a study of natural numbers}},
BOOKTITLE = {TYPES'2000},
EDITOR = {Paul Callaghan and Zhaohui Luo and James McKinna and Randy Pollack},
PUBLISHER = {LNCS, Springer-Verlag},
VOLUME = {2277},
YEAR = {2000},
NOTE = {© Springer-Verlag},
ABSTRACT = {
In type-theory based proof systems that provide inductive structures,
computation tools are automatically associated to inductive
definitions. Choosing a particular representation for a given concept
has a strong influence on proof structure. We propose a method to
make the change from one representation to another easier, by
systematically translating proofs from one context to another. We
show how this method works by using it on natural numbers, for which a
unary representation (based on Peano axioms) and a binary representation
are available. This method leads to an automatic translation tool
that we have implemented in {C}oq and successfully applied to several
arithmetical theorems.
},
URL = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2277&spage=181}
}
@INPROCEEDINGS{MagaudBertot01,
AUTHOR = {N. Magaud and Y. Bertot},
TITLE = {{Changements de Représentation des Structures de Données en Coq: le cas des Entiers Naturels}},
BOOKTITLE = {JFLA'2001},
YEAR = {2001},
NOTE = {Also available as INRIA Research Report \cite{RR4039}},
ABSTRACT = {Dans le calcul des constructions inductives,
des outils de calcul et de preuve sont associés
à chaque type de données concret défini inductivement. Par conséquent, le choix d'une
structure de données influence fortement le contenu des preuves.
Nous proposons dans ce document une méthode pour passer facilement
d'une représentation à une autre, en effectuant des traductions
partiellement automatisées des preuves. Nous mettons cette méthode en
{\oe}uvre sur les entiers naturels, pour lesquels il existe une
représentation unaire (à la Peano) et une représentation binaire.
Un prototype d'outil de traduction est développé dans le système {C}oq et a été
expérimenté avec succès sur une dizaine de théorèmes d'arithmétique.},
URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/JFLA2001.ps.gz}
}
@INPROCEEDINGS{FilliatreMagaud99,
AUTHOR = {Jean-Christophe Filliâtre and Nicolas Magaud},
TITLE = {{Certification of Sorting Algorithms in the Coq System}},
BOOKTITLE = {Theorem Proving in Higher Order Logics:
Emerging Trends},
YEAR = {1999},
ABSTRACT = {We present the formal proofs of total correctness of three sorting
algorithms in the Coq system, namely \textit{insertion sort},
\textit{quicksort} and \textit{heapsort}. The implementations are
imperative programs working in-place on a given array. Those
developments demonstrate the usefulness of inductive types and higher-order
logic in the process of software certification. They also
show that the proof of rather complex algorithms may be done in a
small amount of time --- only a few days for each development ---
and without great difficulty.},
URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/Filliatre-Magaud.ps.gz}
}
@TECHREPORT{RR4475,
AUTHOR = {Yves Bertot and Nicolas Magaud and Paul Zimmermann},
MONTH = {June},
INSTITUTION = {INRIA},
TITLE = {{A Proof of GMP Square Root using the Coq Assistant}},
TYPE = {Research Report 4475},
YEAR = {2002},
URL = {http://www.inria.fr/rrrt/rr-4475.html}
}
@TECHREPORT{RR4039,
AUTHOR = {Nicolas Magaud and Yves Bertot},
INSTITUTION = {INRIA},
TITLE = {{Changements de Repr\'esentation des Donn\'ees dans le Calcul des Constructions Inductives}},
TYPE = {Rapport de recherche 4039},
MONTH = {Octobre},
YEAR = {2000},
URL = {http://www.inria.fr/rrrt/rr-4039.html}
}
@TECHREPORT{Magaud00,
AUTHOR = {Nicolas Magaud},
MONTH = {Juin},
INSTITUTION = {Universit\'e de Nice Sophia-Antipolis},
TITLE = {{Structures de Données Abstraites dans le Calcul des Constructions Inductives}},
TYPE = {Rapport de stage de {DEA}},
YEAR = {2000},
URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/DEA-nmagaud.ps.gz}
}
@TECHREPORT{Magaud99,
AUTHOR = {Nicolas Magaud},
MONTH = {Août},
INSTITUTION = {Ecole Normale Sup\'erieure de Lyon},
TITLE = {{Preuve de Correction d'un Traducteur de Code {Java} vers {JavaCard} dans
le syst{\`e}me {Coq}}},
TYPE = {Rapport de stage de deuxi{\`e}me ann{\'e}e de {M}agist{\`e}re {I}nformatique
et {M}od{\'e}lisation},
YEAR = {1999},
URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/TL.ps.gz}
}
@TECHREPORT{Magaud98,
AUTHOR = {Nicolas Magaud},
MONTH = {Juillet},
INSTITUTION = {Ecole Normale Sup\'erieure de Lyon},
TITLE = {{Preuve de Programmes Imp{\'e}ratifs dans le Syst{\`e}me {Coq} : Tri par Insertion d'un Tableau}},
TYPE = {Rapport de stage de premi{\`e}re ann{\'e}e de {M}agist{\`e}re {I}nformatique
et {M}od{\'e}lisation},
YEAR = {1998},
URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/stageMIM1.ps.gz}
}
This file has been generated by
bibtex2html 1.54