@inproceedings{BM15,
author = {David Braun and Nicolas Magaud},
title = {{Des preuves formelles en Coq du th\'eor\`eme de Thal\`es pour les cercles}},
booktitle = {Vingt-sixi\`emes Journ\'ees Francophones des Langages Applicatifs (JFLA2015)},
year = {2015},
month = {Jan.},
editor = {David Baelde and Jade Alglave},
abstract = {{
Le th\'eor\`eme de Thal\`es pour les cercles et sa r\'eciproque
qui est plus connue sous le nom de th\'eor\`eme du cercle circonscrit \`a un
triangle rectangle sont des propri\'et\'es de g\'eom\'etrie
\'el\'ementaire enseign\'ees dans les coll\`eges fran\c cais.
Nous nous int\'eressons non seulement \`a diff\'erentes descriptions possibles de ces propri\'et\'es en Coq mais aussi aux preuves correspondantes. Nous \'etudions notamment comment le choix d'une repr\'esentation des objets g\'eom\'etriques contenus dans l'\'enonc\'e influencent les arguments de preuve.
Nous pr\'esentons plusieurs approches, une bas\'ee sur des calculs d'angles, une autre bas\'ee sur la g\'eom\'etrie analytique et finalement deux d\'emonstrations diff\'erentes dans l'axiomatique de Tarski en utilisant dans un cas le th\'eor\`eme de la droite des milieux et dans l'autre la notion de sym\'etrie centrale et ses propri\'et\'es.
}},
note = {Proof development available at \url{http://ddbraun.free.fr}},
url = {https://hal.inria.fr/JFLA2015/hal-01099132v1}
}
@article{MCF14,
author = {Nicolas Magaud and Agathe Chollet and Laurent Fuchs},
title = {{Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective}},
journal = {{Annals of Mathematics and Artificial Intelligence}},
publisher = {Springer},
optvolume = 45,
optnumber = 8,
pages = {1--24},
year = {2014},
abstract = {{
This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on previous work by Chollet, Fuchs et al. where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. Laugwitz-Schmieden numbers are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated. In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems.
}},
keywords = {formal proofs, discrete geometry, non-standard arithmetic, arithmetisation scheme, exact computations, Coq},
note = {Online First. To appear. Proof development available at \url{https://dpt-info.u-strasbg.fr/~magaud/Harthong-Reeb/}},
url = {https://hal.inria.fr/hal-01066671}
}
@inproceedings{GeoDis14,
author = {\'Eric Andres and Marie-Andr\'ee Da Col and Laurent Fuchs and Ga\"elle Largeteau-Skapin and Nicolas Magaud and Lo\"\i{}c Mazo and Rita Zrour},
title = {{Les \Omega-AQA : Repr\'esentation discr\`ete des applications affines}},
booktitle = {Neuvi\`emes journ\'ees du Groupe de Travail de G\'eom\'etrie Discr\`ete (G\'eoDis 2014)},
year = {2014},
month = {Nov.},
editor = {Nicolas Passat},
abstract = {{
La droite d'Harthong-Reeb est un mod\`ele num\'erique du continu bas\'e sur les entiers. La construction de cette droite en utilisant les $\Omega$-entiers permet de d\'ecrire les objets math\'ematiques r\'eels de mani\`ere discr\`ete et constructive. En informatique graphique on est souvent amen\'e \`a transformer des objets (images) par des applications affines r\'eelles (rotations, translations, similitudes,\ldots). Des discr\'etis\'es (\`a une \'echelle donn\'ee) de ces applications, appel\'ees applications quasi-affines ont \'et\'e d\'efinies et \'etudi\'ees. Dans ce papier, nous rappelons les d\'efinitions et propri\'et\'es de base des \Omega-entiers, de la droite de Harthong-Reeb et des applications quasi-affines. Nous montrons ensuite comment d\'efinir des $\Omega$-AQAs qui sont les discr\'etis\'es \textsl{multi-\'echelle} des applications affines suivant la th\'eorie des $\Omega$-entiers et la d\'efinition initiale des AQAs. Enfin nous donnons les premi\`eres propri\'et\'es de ces $\Omega$-AQAs.
}},
note = {Presented at ReimsImage'2014 \url{http://reimsimage2014.univ-reims.fr/geodis-2014/sessions/}},
pdf = {http://dpt-info.u-strasbg.fr/~magaud/geodis2014.pdf}
}
@inproceedings{CNVM12,
author = {Bruno Cuervo Parrino and Julien Narboux and Eric Violard and Nicolas Magaud},
title = {Dealing with Arithmetic Overflows in the Polyhedral Model},
booktitle = {2nd International Workshop on Polyhedral Compilation Techniques (IMPACT'2012)},
year = {2012},
month = {Jan.},
editor = {Uday Bondhugula and Vincent Loechner},
note = {Accepted for presentation at the workshop},
abstract = {{
The polyhedral model provides techniques to optimize Static Control Programs (SCoP) using some complex transformations which improve data-locality and which can exhibit parallelism. These advanced transformations are now available in both GCC and LLVM. In this paper, we focus on the correctness of these transformations and in particular on the problem of integer overflows. Indeed, the strength of the polyhedral model is to produce an abstract mathematical representation of a loop nest which allows high-level transformations. But this abstract representation is valid only when we ignore the fact that our integers are only machine integers. In this paper, we present a method to deal with this problem of mismatch between the mathematical and concrete representations of loop nests. We assume the existence of polyhedral optimization transformations which are proved to be correct in a world without overflows and we provide a self-verifying compilation function. Rather than verifying the correctness of this function, we use an approach based on a validator, which is a tool that is run by the compiler after the transformation itself and which confirms that the code produced is equivalent to the original code. As we aim at the formal proof of the validator we implement this validator using the Coq proof assistant as a programming language.
}},
url = {http://hal.inria.fr/hal-00655485/}
}
@inproceedings{BDM12a,
author = {Christophe Brun and Jean-Fran\c cois Dufourd and Nicolas Magaud},
title = {{Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls}},
booktitle = {Automated Deduction in Geometry (ADG'2012) - Revised Selected Papers},
pages = {71-88},
optmonth = {June},
year = {2012},
editor = {Tetsuo Ida and Jacques D. Fleuriot},
volume = {7993},
series = {LNCS},
publisher = {Springer},
abstract = {{This article presents a generic method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification. }},
note = {ISBN 978-3-642-40671-3},
url = {http://hal.inria.fr/hal-00916880}
}
@inproceedings{MCF10,
author = {Nicolas Magaud and Agathe Chollet and Laurent Fuchs},
title = {{Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective}},
booktitle = {Automated Deduction in Geometry (ADG'2010)},
pages = {1-17},
year = {2010},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpublisher = {},
note = {Accepted for presentation at the conference. An extended version is published in an international journal \cite{MCF14}.},
abstract = {{This work presents a formalization of the discrete model of the
continuum introduced by Harthong and Reeb, the
Harthong-Reeb line. This model was at the origin of important
developments in the Discrete Geometry field. The
formalization is based on a previous work by some of the authors where it was shown that the Harthong-Reeb line
satisfies the axioms for constructive real numbers introduced by
Bridges. A formalization of a first attempt for a model
of the Hartong-Reeb line based on the work of Laugwitz and
Schmieden is also presented and analyzed. We hope
that this work could help reasoning and implementation of numeric
computations in geometric systems.
}},
pdf = {http://dpt-info.u-strasbg.fr/~magaud/adg2010-magaud-chollet-fuchs.pdf},
url = {https://dpt-info.u-strasbg.fr/~magaud/Harthong-Reeb/}
}
@article{MNS12,
author = {Nicolas Magaud and Julien Narboux and Pascal Schreck},
title = {{A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem}},
journal = {{Computational Geometry: Theory and Applications}},
publisher = {Elsevier},
volume = 45,
number = 8,
pages = {406--424},
year = {2012},
abstract = {{Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to formalize fairly easily Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.
}},
keywords = {formalization, projective geometry, Coq, rank, desargues, hessenberg, hexamy},
url = {http://hal.inria.fr/inria-00432810/en}
}
@article{BDM12,
author = {Christophe Brun and Jean-Fran\c cois Dufourd and Nicolas Magaud},
title = {{Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq}},
journal = {{Computational Geometry: Theory and Applications}},
publisher = {Elsevier},
volume = 45,
number = 8,
pages = {436-457},
year = {2012},
abstract = {{This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally.
This algorithm, specified in Coq, is then automatically extracted into an OCaml-program which can be plugged into an interface for data input (point selection) and graphical visualization of the output.
A formal proof of total correctness, relying on structural induction, is also carried out.
This requires to study many topologic and geometric properties.
We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane.
Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.}},
url = {http://hal.inria.fr/hal-00955400}
}
@inproceedings{MNS09,
author = {Nicolas Magaud and Julien Narboux and Pascal Schreck},
title = {{Formalizing Desargues' Theorem in Coq using Ranks}},
booktitle = {Proceedings of the ACM Symposium on Applied Computing SAC 2009},
month = {March},
year = {2009},
publisher = {ACM Press},
organization = {ACM},
pages = {1110-1115},
url = {http://hal.inria.fr/inria-00335719},
abstract = {Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions leads to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this paper, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. It allows to carry out proofs in a more systematic way. To validate this approach, we formalize in Coq (using only ranks) one of the fundamental theorems of the projective space, namely Desargues' theorem. }
}
@inproceedings{MNS08,
author = {Nicolas Magaud and Julien Narboux and Pascal Schreck},
title = {{Formalizing Projective Plane Geometry in Coq}},
booktitle = {Post-proceedings of ADG'2008},
optpages = {141--162},
year = {2008},
editor = {Thomas Sturm},
volume = {6301},
number = {},
series = {LNAI},
publisher = {Springer},
abstract = {{We investigate how projective plane geometry can be formalized in a proof assistant such as Coq. Such a formalization increases the reliability of textbook proofs whose details and particular cases are often overlooked and left to the reader as exercises. Projective plane geometry is described through two different axiom systems which are formally proved equivalent. Usual properties such as decidability of equality of points (and lines) are then proved in a constructive way. The duality principle as well as formal models of projective plane geometry are then studied and implemented in Coq. Finally, notions of flats and ranks are introduced and their basic properties are proved. This would allow to develop a more algebraic approach to proofs of alignment properties such as Desargues' theorem.
}},
url = {http://hal.inria.fr/inria-00305998}
}
@inproceedings{CMS08,
author = {Manuel M.T. Chakravarty and Nicolas Magaud and Don Stewart},
title = {{Machine-Independent Code Certification with the LF Type Theory}},
booktitle = {Dependently Typed Programming 08},
year = {2008},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = {Feb.},
optorganization = {},
publisher = {},
note = {A TYPES (small) topical workshop},
url = {http://sneezy.cs.nott.ac.uk/darcs/DTP08/},
abstract = {{Code certification is usually investigated for architecture-dependent
assembly or machine code, where the trusted computing base
(TCB) is minimised at the expense of portability. Work that departs
from that scheme typically focuses on a comparatively high-level
abstract machine code, such as that of the Java Virtual machine.
In contrast, the aim of this work is machine-independent certified
code on a level that is just above that of an architecture-dependent
code. In other words, we aim to minimise the TCB under the over-
ruling aim of portability.
We represent computations as terms of a polymorphic lambda
calculus in administrative normal form, which essentially is a low-
level intermediate language. The type structure of these terms is
embedded in the dependently-typed LF type theory, which serves to
represent certificates. We study how to show the resulting type system
is sound and that the operational semantics of the calculus does not
depend on (dependent) type information. Moreover, we have implemented
a prototype compiler that compiles a small functional language into
certified code as well as a prototype certificate checker based on Twelf.
}}
}
@inproceedings{BDM07,
author = {Christophe Brun and Jean-Fran\c cois Dufourd and Nicolas Magaud},
title = {{Enveloppes convexes et cartes combinatoires en Coq}},
booktitle = {Journ\'ees Informatique et G\'eometrie},
year = {2007},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
address = {INRIA Sophia-Antipolis},
month = {June},
pdf = {http://dpt-info.u-strasbg.fr/~magaud/jig2007.pdf},
url = {http://www-sop.inria.fr/geometrica/events/jig2007/#programme}
}
@misc{Mag05,
author = {Nicolas Magaud},
title = {{Programming with Dependent Types in Coq: a Study of Square Matrices}},
month = {Jan},
year = {2005},
note = {Unpublished. A preliminary version appeared in Coq contributions.},
url = {http://hal.inria.fr/hal-00955444},
abstract = {{The Coq proof system allows users to write (functional) programs and
to reason about them in a formal way. We study how to program using
dependently typed data structures in such a setting. Using dependently
typed data structures enables programmers to have more precise specifications
for their programs before starting proving any significant properties (e.g. total
correctness) about these programs. We particularly focus
on an operational description of square matrices and their operations.
Matrices are represented using dependent types.
A matrix is a vector of rows, which are themselves vectors indexed by natural numbers.
We also take advantage of Coq modules system to have matrices parametrised by a carrier
set. Finally, this operational description of square matrices can be extracted
into a mainstream functional programming language like Ocaml.
}}
}
@inproceedings{Mag04,
author = {Nicolas Magaud},
title = {{Dependently Typed Programming in the Coq Proof Assistant}},
booktitle = {{Dependently Typed Programming: Dagsthul Seminar 04381}},
year = {2004},
address = {Dagsthul},
month = {September},
note = {An overview of the current programming techniques in Coq},
url = {http://dpt-info.u-strasbg.fr/~magaud/Dagsthul04381.MagaudNicolas.Slides.pdf}
}
@phdthesis{Magaud03b,
author = {Nicolas Magaud},
title = {{C}hangements de {R}epr\'esentation des {D}onn\'ees dans le {C}alcul des {C}onstructions},
school = {{U}niversit\'e de Nice Sophia-Antipolis},
year = 2003,
month = oct,
abstract = {{
Nous \'etudions comment faciliter la r\'eutilisation des
preuves formelles en th\'eorie des types. Nous traitons cette question
lors de l'\'etude
de la correction du programme de calcul de la racine carr\'ee de GMP.
A partir d'une description formelle, nous construisons
un programme imp\'eratif avec l'outil Correctness. Cette description
prend en compte tous les d\'etails de l'implantation, y compris
l'arithm\'etique de pointeurs utilis\'ee et la gestion de la m\'emoire. \\
Nous \'etudions aussi comment r\'eutiliser des preuves formelles lorsque
l'on change la repr\'esentation concr\`ete des donn\'ees.
Nous proposons un outil qui permet d'abstraire
les propri\'et\'es calculatoires associ\'ees \`a un type inductif dans
les termes de preuve.
Nous proposons \'egalement des outils pour simuler ces propri\'et\'es
dans un type isomorphe. Nous pouvons ainsi passer, syst\'ematiquement,
d'une repr\'esentation des donn\'ees \`a une autre dans un d\'eveloppement
formel. }},
pdf = {http://dpt-info.u-strasbg.fr/~magaud/papers/TU-0795.pdf},
url = {http://tel.archives-ouvertes.fr/tel-00005903}
}
@inproceedings{Magaud03a,
author = {Nicolas Magaud},
title = {{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem},
booktitle = {TPHOLs'2003},
series = {LNCS},
publisher = {Springer-Verlag},
volume = {2758},
year = {2003},
abstract = {
{In a theorem prover like 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 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 'Arith' library of Coq as well as with
changing polymorphic lists into reversed (snoc) lists. }},
pdf = {http://dpt-info.u-strasbg.fr/~magaud/papers/tphols2003-nmagaud.pdf},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=87}
}
@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.
}}
}
@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://hal.inria.fr/inria-00072113},
note = {Research Report INRIA}
}
@inproceedings{MagaudBertot00,
author = {Nicolas Magaud and Yves Bertot},
title = {{Changing data structures in type theory:a study of natural numbers}},
booktitle = {Post-proceedings of TYPES'2000},
editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Randy Pollack},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {2277},
year = {2002},
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.
},
pdf = {https://dpt-info.u-strasbg.fr/~magaud/papers/types2000-nmagaud.pdf},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2277&spage=181}
}
@inproceedings{MagaudBertot01,
author = {Nicolas Magaud and Yves Bertot},
title = {{Changements de Repr\'esentation des Structures de Donn\'ees 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\'es
\`a chaque type de donn\'ees concret d\'efini inductivement. Par cons\'equent, le choix d'une
structure de donn\'ees influence fortement le contenu des preuves.
Nous proposons dans ce document une m\'ethode pour passer facilement
d'une repr\'esentation \`a une autre, en effectuant des traductions
partiellement automatis\'ees des preuves. Nous mettons cette m\'ethode en
{\oe}uvre sur les entiers naturels, pour lesquels il existe une
repr\'esentation unaire (\`a la Peano) et une repr\'esentation binaire.
Un prototype d'outil de traduction est d\'evelopp\'e dans le syst\`eme {C}oq et a \'et\'e
exp\'eriment\'e avec succ\`es sur une dizaine de th\'eor\`emes d'arithm\'etique.},
url = {http://dpt-info.u-strasbg.fr/~magaud/INRIA/FTP/JFLA2001.pdf}
}
@inproceedings{FilliatreMagaud99,
author = {Jean-Christophe Filli\^atre 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 = {http://dpt-info.u-strasbg.fr/~magaud/INRIA/FTP/Filliatre-Magaud.pdf}
}
@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://hal.inria.fr/inria-00072599}
}
@techreport{Magaud00,
author = {Nicolas Magaud},
month = {Juin},
institution = {Universit\'e de Nice Sophia-Antipolis},
title = {{Structures de Donn\'ees Abstraites dans le Calcul des Constructions Inductives}},
type = {Rapport de stage de {DEA}},
year = {2000},
url = {http://dpt-info.u-strasbg.fr/~magaud/INRIA/FTP/DEA-nmagaud.pdf}
}
@techreport{Magaud99,
author = {Nicolas Magaud},
month = {Ao\^ut},
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 = {http://dpt-info.u-strasbg.fr/~magaud/INRIA/FTP/TL.pdf}
}
@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 = {http://dpt-info.u-strasbg.fr/~magaud/INRIA/FTP/stageMIM1.pdf}
}
This file was generated by bibtex2html 1.98.