| [1] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
Certification of automated termination proofs.
In Proc.of 6th International Symposium on Frontiers of
Combining Systems, Lecture Notes in Artificial Intelligence, Liverpool,UK,
2007. Springer-Verlag (to appear).
[ bib ]
(Voir le résumé)
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 check the soundness of a
proof, they lack automation. Regarding automated tools,
one still has to be satisfied with their answers
Yes/No/Donotknow, 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.
|
| [2] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
Certification of automated termination proofs.
Rapport scientifique 1185, Cedric, 2007.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
A preliminary version of [1].
|
| [3] |
Brigitte Grau, Anne-Laure Ligozat, Isabelle Robba, Anne Vilnat, Faza El
Kateb, Gabriel Illouz, Laura Monceaux, Patrick Paroubek, and Olivier Pons.
De l'importance des synonymes pour la sélection de passages en
question-réponse.
In Conférence en Recherche d'Informations et Applications
(CORIA'05), pages 71-84, mars 2005.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [4] |
Brigitte Grau, Gabriel Illouz, Laura Monceaux, Patrick Paroubek, Olivier Pons,
Isabelle Robba, and Anne Vilnat.
Frasques, le système du groupe lir, limsi.
In Atelier EQueR, Conférence (TALN'05), pages 85-88, juin
2005.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [5] |
Catherine Dubois, Mathieu Jaume, Olivier Pons, and Virgile Prevosto.
L'atelier focal.
In Actes du Congrès AFADL'04, Approches Formelles dans
l'Assistance au Développement de Logiciels (Session Outils), Besancon,
France, June 2004.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [6] |
Gilles Barthe, Venanzio Capretta, and Olivier Pons.
Setoids in type theory.
J. Funct. Program., 13(2):261-293, 2003.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [7] |
Gilles Barthe and Olivier Pons.
Type isomorphisms and proof reuse in dependent type theory.
In Furio Honsell and Marino Miculan, editors, FoSSaCS, volume
2030 of Lecture Notes in Computer Science, pages 57-71. Springer,
2001.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
We propose a theoretical foundation for proof reuse,
based on the novel idea of a computational interpretation of
type isomorphisms.
|
| [8] |
Olivier Pons.
Generalization in type theory based proof assistants.
In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack,
editors, TYPES, volume 2277 of Lecture Notes in Computer Science,
pages 217-232. Springer, December 2000.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [9] |
Yves Bertot, Olivier Pons, and Loïc Pottier.
Graphes de dépendance pour les démonstrateurs de théorèmes
intéractifs.
Technical Report RR-4052, Institut National de Recherche en
Informatique et en Automatique (INRIA), November 2000.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
(Voir le résumé)
Keywords: Dependency graphs theorems proof Coq GraphViz daVinci
|
| [10] |
Olivier Pons.
Proof engineering.
Rapport de recherche, aboratoire CEDRIC-CNRAM, September 2000.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [11] |
Olivier Pons.
Proof generalization and proof reuse.
In J. Harrison M. Aagaard and T. Schubert, editors,
Supplementary Proceedings of the 13th International Conference on Theorem
Proving in Higher Order Logics: Poster session TPHOLs'00, Portland U.S.,
August 2000. Oregon Graduate Institute Technical Report CSE 00-009.
[ bib ]
(Voir le résumé)
|
| [12] |
Olivier Pons.
Ingénierie de preuve.
In INRIA, editor, Actes des Journées francophones des langages
applicatifs 2000, pages 171 - 186, Mont Saint-Michel, France, January 2000.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [13] |
Olivier Pons.
Conception et réalisation d'outils d'aide au développement
de grosses théories dans les systèmes de preuves interactifs.
PhD thesis, Conservatoire National des Arts et Métiers, Paris,
France, July 1999.
[ bib |
.ps.gz ]
(Voir le résumé)
|
| [14] |
Olivier Pons, Yves Bertot, and Laurence Rideau.
Notions of dependency in proof assistants.
In Electronic Proceedings of User Interfaces for Theorem
Provers 1998, Sophia-Antipolis, France, July 1998.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
This article describes uses of dependencies in tools to maintain big proofs in interactive proof assistants.
|
| [15] |
Olivier Pons.
Undoing and managing a proof.
In Electronic Proceedings of User Interfaces for Theorem
Provers 1997, Sophia-Antipolis, France, September 1997.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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.
|
| [16] |
Olivier Pons.
Vers une formalisation de l'algèbre relationel en coq.
Rapport de dea, Université Pierre et Marie Curie - Paris 6, Paris,
France, September 1995.
[ bib |
.pdf |
.ps.gz ]
(Voir le résumé)
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 !
|
Ce fichier a été généré par bibtex2html 1.82.
Dernière mise-à-jour ven jun 8 12:05:31 CEST 2007