@MASTERSTHESIS{OP:Dea,
AUTHOR = {Olivier Pons},
TITLE = {Vers une formalisation de l'algèbre relationel en Coq},
SCHOOL = {Université Pierre et Marie Curie - Paris 6},
YEAR = {1995},
TYPE = {Rapport de DEA},
ADDRESS = {Paris, France},
MONTH = SEP,
ABSTRACT = {
C'est complètement dépassé et j'ai un peu honte mais ça peut remonter
le moral de ceux qui ont du mal en DEA !
},
URL = {http://www.ensiie.fr/~pons/PAPERS/ponsDEA.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/ponsDEA.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {dea}
}
@INPROCEEDINGS{conf/uitp/Pons97,
AUTHOR = {Olivier Pons},
TITLE = {Undoing and Managing a proof},
BOOKTITLE = {Electronic Proceedings of "User Interfaces for Theorem Provers 1997"},
ADDRESS = {Sophia-Antipolis, France},
MONTH = SEP,
YEAR = 1997,
ABSTRACT = {
In this paper we work in the area of proof script
management. We study the dependencies between commands
in a script and how they can be exploited in the undoing
process. We present some problems that we have met in
our implementa tion of proof managing tools in the Ctcoq
interface for the Coq System. },
URL = {http://www.ensiie.fr/~pons/PAPERS/uitp97.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/uitp97.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {icolcomlec}
}
@INPROCEEDINGS{conf/uitp/PonsBertotRideau98,
AUTHOR = {Olivier Pons and Yves Bertot and Laurence Rideau},
TITLE = {Notions of dependency in proof assistants},
BOOKTITLE = {Electronic Proceedings of "User Interfaces for Theorem Provers 1998"},
ADDRESS = {Sophia-Antipolis, France},
MONTH = JUL,
YEAR = 1998,
ABSTRACT = {
This article describes uses of dependencies in tools to
maintain big proofs in interactive proof assistants.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/uitp98.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/uitp98.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {icolcomlec}
}
@PHDTHESIS{OP:These,
AUTHOR = {Olivier Pons},
TITLE = {Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosses th\'eories dans les syst\`emes de preuves interactifs},
SCHOOL = {Conservatoire National des Arts et M\'etiers},
YEAR = {1999},
ADDRESS = {Paris, France},
MONTH = JUL,
ABSTRACT = {
},
PS = {http://www.ensiie.fr/~pons/PAPERS/these.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {these}
}
@INPROCEEDINGS{conf/jfla/Pons2000,
AUTHOR = {Olivier Pons},
TITLE = {Ingénierie de preuve},
OPTCROSSREF = {},
BOOKTITLE = {Actes des Journées francophones des langages applicatifs 2000},
PAGES = {171 - 186 },
YEAR = {2000},
EDITOR = {INRIA},
ADDRESS = {Mont Saint-Michel, France },
MONTH = JAN,
ABSTRACT = {
L'objet de cet article est de présenter un panorama
d'outils d'analyses et de manipulations de preuves
formelles. Le but des outils proposés est de faciliter
le développement et la maintenance de théories dans les
assistants de preuve afin d'améliorer la productivité
des utilisateurs de ces systèmes.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/jfla2000.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/jfla2000.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {ncolcomlec}
}
@INPROCEEDINGS{conf/suptphol/Pons2000,
AUTHOR = { Olivier Pons },
TITLE = { Proof generalization and proof reuse },
BOOKTITLE = { Supplementary Proceedings of the 13th International
Conference on Theorem Proving in Higher Order Logics: Poster session
TPHOLs'00},
MONTH = AUG,
EDITOR = {M. Aagaard, J. Harrison and T. Schubert},
PUBLISHER = {Oregon Graduate Institute Technical Report CSE 00-009 },
ADDRESS = {Portland U.S.},
YEAR = {2000},
PAGES = { },
ABSTRACT = {
}
}
@TECHREPORT{RR/Pons00,
AUTHOR = {Olivier Pons},
TITLE = {Proof engineering},
INSTITUTION = {aboratoire CEDRIC-CNRAM},
YEAR = {2000},
TYPE = {Rapport de Recherche},
MONTH = SEP,
OPTNUMBER = {},
ABSTRACT = { The main purpose of this article is to present a
panorama of tools for formal proof analysis and
management. The proposed tools are based upon several
notions of dependency. Our principal objective is to
facilitate the development and the maintenance of
theories in proofs assistants in order to improve the
productivity of such systems' users.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/RR-Cedric00.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/RR-Cedric00.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {rapport}
}
@TECHREPORT{RR/Bertot/Pons/Pottier00,
AUTHOR = {Yves Bertot and Olivier Pons and Loïc Pottier},
TITLE = {Graphes de dépendance pour les démonstrateurs de théorèmes intéractifs},
INSTITUTION = {Institut National de Recherche en Informatique et en Automatique (INRIA)},
YEAR = {2000},
MONTH = NOV,
NUMBER = {RR-4052},
KEYWORDS = {Dependency graphs theorems proof Coq GraphViz daVinci
},
ABSTRACT = { We propose tools to visualize large proof developments
as graphs of theorems and definitions where edges
denote the dependency between two theorems. In
particular, we study means to limit the size of
graphs. Experiments have been done with the Coq theorem
prover and the GraphViz and daVinci graph visualization
suites.
},
RESUME = { Nous proposons dans ce rapport des outils pour visualiser
de grandes preuves sous forme de graphes de théorèmes et
de définitions, où les arrêtes dénotent les dépendances
entre deux théorèmes. En particulier, on étudie les
moyens de limiter la taille de ces graphes. Nous avaons
mené les expérimentations à l'aide des systèmes Coq,
GraphViz et daVinci.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/RR-4052.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/RR-4052.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {rapport}
}
@INPROCEEDINGS{conf/fossacs/BartheP01,
AUTHOR = {Gilles Barthe and
Olivier Pons},
TITLE = {Type Isomorphisms and Proof Reuse in Dependent Type Theory.},
BOOKTITLE = {FoSSaCS},
YEAR = {2001},
PAGES = {57-71},
EE = {http://link.springer.de/link/service/series/0558/bibs/2030/20300057.htm},
CROSSREF = {conf/fossacs/2001},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de},
ABSTRACT = { We propose a theoretical foundation for proof reuse,
based on the novel idea of a computational interpretation of
type isomorphisms.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/fossacs01.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/fossacs01.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {icolcomlec}
}
@PROCEEDINGS{conf/fossacs/2001,
EDITOR = {Furio Honsell and
Marino Miculan},
TITLE = {Foundations of Software Science and Computation Structures,
4th International Conference, FOSSACS 2001 Held as Part
of the Joint European Conferences on Theory and Practice
of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001,
Proceedings},
BOOKTITLE = {FoSSaCS},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2030},
YEAR = {2001},
ISBN = {3-540-41864-4},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@INPROCEEDINGS{conf/types/Pons00,
AUTHOR = {Olivier Pons},
TITLE = {Generalization in Type Theory Based Proof Assistants.},
BOOKTITLE = {TYPES},
YEAR = {2000},
MONTH = DEC,
PAGES = {217-232},
EE = {http://link.springer.de/link/service/series/0558/bibs/2277/22770217.htm},
CROSSREF = {conf/types/2000},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de},
ABSTRACT = { This paper describes a mechanism to generalize
mathematical results in type theory based proof
assistants. The proposed mechanism starts from a proved
theorem or a proved set of theorems (a theory) and
makes it possible to get less specific results that can
be instantiated and reused in other contexts.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/types00.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/types00.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {icolcomlec}
}
@PROCEEDINGS{conf/types/2000,
EDITOR = {Paul Callaghan and
Zhaohui Luo and
James McKinna and
Robert Pollack},
TITLE = {Types for Proofs and Programs, International Workshop, TYPES
2000, Durham, UK, December 8-12, 2000, Selected Papers},
BOOKTITLE = {TYPES},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2277},
YEAR = {2002},
ISBN = {3-540-43287-6},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@ARTICLE{journals/jfp/BartheCP03,
AUTHOR = {Gilles Barthe and Venanzio Capretta and Olivier Pons},
TITLE = {Setoids in type theory.},
JOURNAL = {J. Funct. Program.},
VOLUME = {13},
NUMBER = {2},
YEAR = {2003},
PAGES = {261-293},
EE = {http://dx.doi.org/10.1017/S0956796802004501},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de},
ABSTRACT = { Formalising mathematics in dependent type theory often
requires to represent sets as setoids, i.e. types with
an explicit equality relation. This paper surveys some
possible definitions of setoids and assesses their
suitability as a basis for developing
mathematics. According to whether the equality relation
is required to be reflexive or not we have total or
partial setoid, respectively. There is only one
definition of total setoid, but four different
definitions of partial setoid, depending on four
different notions of setoid function. We prove that one
approach to partial setoids in unsuitable, and that the
other approaches can be divided in two classes of
equivalence. One class contains definitions of partial
setoids that are equivalent to total setoids; the other
class contains an inherently different definition, that
has been useful in the modeling of type systems. We
also provide some elements of discussion on the merits
of each approach from the viewpoint of formalizing
mathematics. In particular, we exhibit a difficulty
with the common definition of subsetoids in the partial
setoid approach.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/setoid.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/setoid.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {irevcomlec}
}
@INPROCEEDINGS{conf/afadl/DuboisJaumePonsPrevosto2004,
AUTHOR = {Catherine Dubois and Mathieu Jaume and Olivier Pons and Virgile Prevosto},
TITLE = {L'atelier FOCAL},
BOOKTITLE = {Actes du Congr\`es AFADL'04, Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels (Session Outils)},
PAGES = {},
ADDRESS = {Besancon, France},
MONTH = JUN,
YEAR = 2004,
ABSTRACT = { L'atelier FOCAL est un atelier intégré de construction
modulaire de logiciels certifiés. Il permet l'écriture
de modules constitués de déclarations, définitions,
énoncés et preuves. Les déclarations peuvent être
raffinées en définitions et les énoncés en preuves, par
passage progressif de la spécification à l'implantation,
à l'aide de mécanismes d'héritage, de redéfinition et
d'instanciation de paramètres génériques. La compilation
des modules développés avec l'atelier FOCAL produit un
code exécutable OCaml et un développement formel Coq.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/Focal-afadl2004.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/Focal-afadl2004.ps.gz},
TOPICS = {team},
TYPE_PUBLI = {ncolcomlec}
}
@INPROCEEDINGS{graucoria05,
AUTHOR = {Brigitte Grau and Anne-Laure Ligozat and Isabelle Robba and Anne Vilnat and Fa\îza El Kateb and Gabriel Illouz and Laura Monceaux and Patrick Paroubek and Olivier Pons},
TITLE = {De l'importance des synonymes pour la sélection de passages en question-réponse},
BOOKTITLE = {Conférence en Recherche d'Informations et Applications (CORIA'05)},
MONTH = {mars},
PAGES = {71-84},
YEAR = {2005},
TOPICS = {team},
ABSTRACT = {Les systèmes de question-réponse développés actuellement adoptent pour
la plupart et à peu de chose près le même type d'architecture que l'on
peut schématiser en trois modules : l'analyse de la question, la
sélection des documents, l'extraction de la réponse. Mais ce en quoi
ils diffèrent, ce sont les outils (moteur d'indexation, analyseurs...)
et les bases de connaissances qu'ils utilise nt. Pour chacun de ces
systèmes, il est donc important d'évaluer l'apport de ces
outils ou bases de connaissances. Dans le cadre de la campagne Equer
(campagne d'évaluation des systèmes de question-réponse pour le
français), notre système F RASQUES a produit deux jeux de résultats :
l'un utilise des synonymes dans les b i-termes, l'autre pour les
mono-termes aussi. La comparaison de ces deux tests e t l'étude d'un
corpus plus large, en français et en anglais, permet de mesurer l'apport
de ces connaissances sémantiques.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/cauria-grau.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/cauriaègrau.ps.gz}
}
@INPROCEEDINGS{grautaln05,
AUTHOR = {Brigitte Grau and Gabriel Illouz and Laura Monceaux and Patrick Paroubek and Olivier Pons and Isabelle Robba and Anne Vilnat},
TITLE = {FRASQUES, le système du groupe LIR, LIMSI},
BOOKTITLE = {Atelier EQueR, Conférence (TALN'05)},
MONTH = {juin},
PAGES = {85-88},
YEAR = {2005},
TOPICS = {team},
ABSTRACT = {
Le système FRASQUES qui a participé à l'évaluation EQueR
est présenté ici en comparaison avec le système QUALC dédié
à l'anglais. Ses Résultats sont commentés en une évaluation
des différents modules est exposée.
We Present our system FRASQUES in comparison to QUALC our
systeme for English. The results that FRASQUES obtained at
EqueR are presented, and an évaluation of its modules is
given.
},
URL = {http://www.ensiie.fr/~pons/PAPERS/Frasque.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/Frasque.ps.gz}
}
@INPROCEEDINGS{conf/frocos/a3pat2007,
AUTHOR = {Évelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
TITLE = {Certification of automated termination proofs},
EDITOR = {},
BOOKTITLE = {Proc.\ of 6th International Symposium on Frontiers of Combining Systems},
SERIES = {Lecture Notes in Artificial Intelligence},
OPTVOLUME = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag (to appear)},
ADDRESS = {Liverpool,UK},
YEAR = {2007},
ABSTRACT = {
Nowadays, formal methods rely on tools of different kinds:
proof assistants with which the user interacts to discover
a proof step by step; and fully automated tools which make
use of (intricate) decision procedures. But while some
proof assistants can \emph{check} the soundness of a
proof, they lack automation. Regarding automated tools,
one still has to be satisfied with their answers
\texttt{Yes}/\texttt{No}/\texttt{Do\,not\,know}, the
validity of which can be subject to question, in
particular because of the increasing size and complexity
of these tools.
In the context of rewriting techniques, we aim at bridging
the gap between proof assistants that yield formal
guarantees of reliability and highly automated tools one
has to trust. We present an approach making use of both
shallow and deep embeddings. We illustrate this approach
with a prototype based on the CiME rewriting toolbox,
which can discover involved termination proofs that can be
certified by the Coq proof assistant, using the Coccinelle
library for rewriting.
}
}
@TECHREPORT{rap/cedric/a3pat2007,
AUTHOR = {Évelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
TITLE = {Certification of automated termination proofs},
INSTITUTION = {Cedric},
YEAR = {2007},
OPTKEY = {},
TYPE = {Rapport scientifique},
NUMBER = {1185},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
URL = {http://www.ensiie.fr/~pons/PAPERS/RC1185.pdf},
PS = {http://www.ensiie.fr/~pons/PAPERS/RC1185.ps.gz},
ABSTRACT = {A preliminary version of \cite{conf/frocos/a3pat2007}. }
}
This file has been generated by bibtex2html 1.82.
Dernière mise-à-jour ven jun 8 12:05:31 CEST 2007