Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
publis.bib
@MISC{BoldoFilliatre06,
author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
title = {{Formal Verification of Floating-Point Programs}},
month = {October},
year = 2006,
note = {Submitted for publication},
url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.ps},
abstract = {
This paper introduces a methodology to perform formal verification
of floating-point C programs. It extends an existing tool for the
verification of C programs, Caduceus, with new annotations specific
to floating-point arithmetic. The Caduceus first-order logic model
for C programs is extended accordingly. Then verification conditions
expressing the correctness of the programs are obtained in the usual
way and can be discharged interactively with the Coq proof
assistant, using an existing Coq formalization of floating-point
arithmetic. This methodology is already implemented and has been
successfully applied to several short floating-point programs, which
are presented in this paper.}
}
@MISC{ConchonFilliatre06c,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{A Persistent Union-Find Data Structure}},
year = 2006,
note = {English version of \cite{ConchonFilliatre06b}},
url = {http://www.lri.fr/~filliatr/ftp/publis/puf-rr.ps.gz},
abstract = {
The problem of disjoint sets, also known as \emph{union-find},
consists in maintaining a partition of a finite set into a data
structure. This structure provides two operations: a function
\emph{find} returning the class of an element and a function
\emph{union} merging two classes. An optimal and imperative solution
is known since 1975 and is due to Tarjan.
However, the imperative nature of this data structure may be a
drawback when it is used in a backtracking algorithm. This paper
details the implementation of a persistent union-find data structure
which appears to be almost as efficient as its imperative counterpart.
To reach this efficiency, our solution makes heavy use of imperative
features. This is why we also detail a formal proof of correctness,
which especially shows the persistent nature of this solution.
}
}
@MISC{ConchonFilliatre06b,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Union-Find Persistant}},
year = 2006,
note = {Soumis},
url = {http://www.lri.fr/~filliatr/ftp/publis/puf.ps.gz},
abstract = {
Le problème des classes disjointes, connu sous le nom de
\emph{union-find}, consiste à maintenir dans une structure de
données une partition d'un ensemble fini. Cette structure fournit deux
opérations : une fonction \emph{find} déterminant la classe d'un
élément et une fonction \emph{union} réunissant deux classes. Une
solution optimale et impérative, due à Tarjan, est connue depuis
longtemps.
Cependant, le caractère impératif de cette structure de données
devient gênant lorsqu'elle est utilisée dans un contexte où
s'effectuent des retours en arrière (\emph{backtracking}). Nous
présentons dans cet article une version persistante de
\emph{union-find} dont la complexité est comparable à celle de la
solution impérative. Pour obtenir cette efficacité, notre solution
utilise massivement des traits impératifs. C'est pourquoi nous
présentons également une preuve formelle de correction, pour
s'assurer notamment du caractère persistant de cette solution.
}
}
@INPROCEEDINGS{ConchonFilliatre06,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
title = {{Type-Safe Modular Hash-Consing}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
note = {Supersedes~\cite{Filliatre00b}},
month = {September},
year = 2006,
url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz},
abstract = {
Hash-consing is a technique to share values that are structurally
equal. Beyond the obvious advantage of saving memory blocks,
hash-consing may also be used to speedup fundamental operations and
data structures by several orders of magnitude when sharing is
maximal. This paper introduces an Ocaml hash-consing library that
encapsulates hash-consed terms in an abstract datatype, thus safely
ensuring maximal sharing. This library is also parameterized by an
equality that allows the user to identify terms according to an
arbitrary equivalence relation.}
}
@UNPUBLISHED{ocamlgraphGPCE,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
title = {{Designing a Generic Graph Library using ML Functors}},
note = {Submitted for publication},
month = {May},
year = 2006,
url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph.ps},
abstract = {
This article details the design and implementation of Ocamlgraph, a
generic graph library for the programming language Ocaml. This
library features a large set of graph data structures---directed or
undirected, with or without labels on vertices and edges, as persistent
or mutable data structures, etc.---and a large set of graph
algorithms written independently of the graph data structure. Such a
genericity is obtained through a massive use of \ocaml module system
and of its functions, the so-called \emph{functors}.}
}
@UNPUBLISHED{AyacheFilliatre06,
author = {Nicolas Ayache and Jean-Christophe Filli\^atre},
title = {{Combining the Coq Proof Assistant with First-Order Decision Procedures}},
note = {Unpublished},
month = {March},
year = 2006,
url = {http://www.lri.fr/~filliatr/publis/coq-dp.ps.gz},
abstract = {
We present an integration of first-order automatic theorem provers
into the Coq proof assistant. This integration is based on a
translation from the higher-order logic of Coq, the Calculus of
Inductive Constructions, to a polymorphic first-order logic. This
translation is defined and proved sound in this paper. It includes
not only the translation of terms and predicates belonging to the
first-order fragment, but also several techniques to go well
beyond: abstractions of higher-order sub-terms, case-analysis,
mutually recursive functions and inductive types.
This process has been implemented in the Coq proof assistant to call
the decision procedures Simplify, CVC Lite, haRVey and Zenon through
Coq tactics. The first experiments are promising.}
}
@INPROCEEDINGS{Filliatre06,
author = {Jean-Christophe Filli\^atre},
title = {{Backtracking iterators}},
booktitle = {ACM SIGPLAN Workshop on ML},
address = {Portland, Oregon},
note = {{Also LRI Research Report 1428}},
month = SEP,
year = {2006},
note = {English translation of \cite{Filliatre05}.},
url = {http://www.lri.fr/~filliatr/publis/enum2.ps.gz},
abstract = {
Iterating over the elements of an abstract collection is usually
done in ML using a fold-like higher-order function provided by the
data structure. This article discusses a different paradigm of
iteration based on purely functional, immutable cursors. Contrary
to fold-like iterators, the iteration can be cleanly interrupted at
any step. Contrary to imperative cursors (such as those found in C++
and Java libraries) it is possible to backtrack the iterator to a
previous step. Several ways to iterate over binary trees are
examined and close links with G\'erard Huet's Zipper are
established. Incidentally, we show the well-known two-lists
implementation of functional queues arising from a Zipper-based
breadth-first traversal.}
}
@INPROCEEDINGS{Filliatre05,
author = {Jean-Christophe Filli\^atre},
title = {{Itérer avec persistance}},
booktitle = {Dix-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
year = 2006,
address = {Pauillac, France},
publisher = {INRIA},
url = {http://www.lri.fr/~filliatr/publis/enum.ps.gz},
abstract = {
L'énumération des éléments d'une structure de données est
généralement réalisée en ML par l'intermédiaire d'une fonction
d'ordre supérieur. Cet article présente une alternative, sous la
forme d'itérateurs pas à pas, à l'instar de ce qui se fait en
programmation orientée objets, mais basés sur des structures
persistantes, de manière à permettre notamment un éventuel
\emph{backtracking}. Plusieurs façons de parcourir les arbres
binaires sont examinées, et des liens étroits avec le Zipper de
Gérard Huet sont établis.}
}
@MISC{TypesSummerSchool2005,
author = {Jean-Christophe Filli\^atre},
title = {{Program Verification using Coq. Introduction to the WHY tool}},
year = 2005,
note = {Lecture Notes, TYPES Summer School 2005 (Göteborg, Sweden)},
month = AUG,
url = {http://www.lri.fr/~filliatr/publis/tss-2005.ps.gz}
}
@MISC{ipf,
author = {Jean-Christophe Filli\^atre},
title = {{Introduction à la programmation fonctionnelle}},
year = 2004,
note = {Notes de cours de Master M1},
url = {http://www.lri.fr/~filliatr/publis/ipf.ps.gz}
}
@INPROCEEDINGS{ConchonFilliatreSignoles05,
author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien Signoles},
title = {Le foncteur sonne toujours deux fois},
booktitle = {Seizi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = MAR,
year = 2005,
publisher = {INRIA},
url = {http://www.lri.fr/~filliatr/ftp/publis/jfla05.ps.gz},
abstract = { Cet article présente Ocamlgraph, une bibliothèque générique de graphes pour
le langage de programmation Ocaml. L'originalité de cette
bibliothèque est de proposer d'une part un grand nombre de
structures de données différentes pour représenter les graphes ---
graphes orientés ou non, structures persistantes ou modifiées en
place, sommets et arcs avec ou sans étiquettes, marques sur les
sommets, etc. --- et d'autre part des algorithmes sur les graphes
écrits indépendamment de la structure de données représentant les
graphes. Le codage de ces deux aspects originaux a été rendu
possible par une utilisation massive du système de modules d'Ocaml
et notamment de ses fonctions, les foncteurs.
}
}
@INPROCEEDINGS{FilliatreMarche04,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {{Multi-Prover Verification of C Programs}},
booktitle = {Sixth International Conference on
Formal Engineering Methods (ICFEM)},
year = 2004,
address = {Seattle},
month = NOV,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 3308,
pages = {15--29},
url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus.ps.gz},
abstract = {
Our goal is the verification of C programs at the source code level
using formal proof tools. Programs are specified using annotations such
as pre- and postconditions and global invariants. An
original approach is presented which allows to formally prove that a
function implementation satisfies its specification and is free of
null pointer dereferencing and out-of-bounds array access.
The method is not bound to a particular back-end theorem prover. A
significant part of the ANSI C language is supported, including
pointer arithmetic and possible pointer aliasing. We describe a
prototype tool and give some experimental results.}
}
@INPROCEEDINGS{FilliatreLetouzey03,
author = {J.-C. Filli\^atre and P. Letouzey},
title = {{Functors for Proofs and Programs}},
booktitle = {Proceedings of The European Symposium on Programming},
year = 2004,
address = {Barcelona, Spain},
month = {April},
series = {Lecture Notes in Computer Science},
volume = 2986,
pages = {370--384},
url = {http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz},
abstract = {
This paper presents the formal verification with the Coq proof assistant of
several applicative data structures implementing finite sets.
These implementations are parameterized by an ordered type for the
elements, using functors from the ML module system. The verification
follows closely this scheme, using the newly Coq module system.
One of the verified implementation is the actual code for sets and
maps from the Objective Caml standard library.
The formalization refines the informal specifications of these
libraries into formal ones. The process of
verification exhibited two small errors in the balancing scheme,
which have been fixed and then verified.
Beyond these verification results, this article illustrates the use
and benefits of modules and functors in a logical framework.
}
}
@TECHREPORT{Filliatre03,
author = {J.-C. Filli\^atre},
title = {{Why: a multi-language multi-prover verification tool}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = {1366},
month = {March},
year = 2003,
url = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
}
@ARTICLE{FilliatrePottier02,
author = {J.-C. Filli{\^a}tre and F. Pottier},
title = {{Producing All Ideals of a Forest, Functionally}},
journal = {Journal of Functional Programming},
volume = 13,
number = 5,
pages = {945--956},
month = {September},
year = 2003,
url = {http://www.lri.fr/~filliatr/ftp/publis/kr-fp.ps.gz},
abstract = {
We present a functional implementation of Koda and Ruskey's
algorithm for generating all ideals of a forest poset as a Gray
code. Using a continuation-based approach, we give an extremely
concise formulation of the algorithm's core. Then, in a number of
steps, we derive a first-order version whose efficiency is
comparable to a C implementation given by Knuth.}
}
@UNPUBLISHED{FORS01,
author = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
title = {Deciding Propositional Combinations of Equalities and Inequalities},
note = {Unpublished},
month = OCT,
year = 2001,
url = {http://www.lri.fr/~filliatr/ftp/publis/ics.ps},
abstract = {
We address the problem of combining individual decision procedures
into a single decision procedure. Our combination approach is based
on using the canonizer obtained from Shostak's combination algorithm
for equality. We illustrate our approach with a combination
algorithm for equality, disequality, arithmetic inequality, and
propositional logic. Unlike the Nelson--Oppen combination where the
processing of equalities is distributed across different closed
decision procedures, our combination involves the centralized
processing of equalities in a single procedure. The termination
argument for the combination is based on that for Shostak's
algorithm. We also give soundness and completeness arguments.}
}
@INPROCEEDINGS{ICS,
author = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
title = {{ICS: Integrated Canonization and Solving (Tool presentation)}},
booktitle = {Proceedings of CAV'2001},
editor = {G. Berry and H. Comon and A. Finkel},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 2102,
pages = {246--249},
year = 2001
}
@INPROCEEDINGS{Filliatre01a,
author = {J.-C. Filli\^atre},
title = {La supériorité de l'ordre supérieur},
booktitle = {Journées Francophones des Langages Applicatifs},
pages = {15--26},
month = {Janvier},
year = 2002,
address = {Anglet, France},
url = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz},
code = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps},
abstract = {
Nous présentons ici une écriture fonctionnelle de l'algorithme de
Koda-Ruskey, un algorithme pour engendrer une large famille
de codes de Gray. En s'inspirant de techniques de programmation par
continuation, nous aboutissons à un code de neuf lignes seulement,
bien plus élégant que les implantations purement impératives
proposées jusqu'ici, notamment par Knuth. Dans un second temps,
nous montrons comment notre code peut être légèrement modifié pour
aboutir à une version de complexité optimale.
Notre implantation en Objective Caml rivalise d'efficacité avec les
meilleurs codes C. Nous détaillons les calculs de complexité,
un exercice intéressant en présence d'ordre supérieur et d'effets de
bord combinés.}
}
@TECHREPORT{Filliatre00c,
author = {J.-C. Filli\^atre},
title = {{Design of a proof assistant: Coq version 7}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = {1369},
month = {October},
year = 2000,
url = {http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz},
abstract = {
We present the design and implementation of the new version of the
Coq proof assistant. The main novelty is the isolation of the
critical part of the system, which consists in a type checker for
the Calculus of Inductive Constructions. This kernel is now
completely independent of the rest of the system and has been
rewritten in a purely functional way. This leads to greater clarity
and safety, without compromising efficiency. It also opens the way to
the ``bootstrap'' of the Coq system, where the kernel will be
certified using Coq itself.}
}
@TECHREPORT{Filliatre00b,
author = {J.-C. Filli\^atre},
title = {{Hash consing in an ML framework}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = {1368},
month = {September},
year = 2000,
url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing.ps.gz},
abstract = {
Hash consing is a technique to share values that are structurally
equal. Beyond the obvious advantage of saving memory blocks, hash
consing may also be used to gain speed in several operations (like
equality test) and data structures (like sets or maps) when sharing is
maximal. However, physical adresses cannot be used directly for this
purpose when the garbage collector is likely to move blocks
underneath. We present an easy solution in such a framework, with
many practical benefits.}
}
@MISC{ocamlweb,
author = {J.-C. Filli\^atre and C. March\'e},
title = {{ocamlweb, a literate programming tool for Objective Caml}},
note = {Available at \url{http://www.lri.fr/~filliatr/ocamlweb/}},
url = {http://www.lri.fr/~filliatr/ocamlweb/}
}
@ARTICLE{Filliatre00a,
author = {J.-C. Filli\^atre},
title = {{Verification of Non-Functional Programs
using Interpretations in Type Theory}},
journal = {Journal of Functional Programming},
volume = 13,
number = 4,
pages = {709--745},
month = {July},
year = 2003,
note = {English translation of~\cite{Filliatre99}.},
url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
abstract = {We study the problem of certifying programs combining imperative and
functional features within the general framework of type theory.
Type theory constitutes a powerful specification language, which is
naturally suited for the proof of purely functional programs. To
deal with imperative programs, we propose a logical interpretation
of an annotated program as a partial proof of its specification. The
construction of the corresponding partial proof term is based on a
static analysis of the effects of the program, and on the use of
monads. The usual notion of monads is refined in order to account
for the notion of effect. The missing subterms in the partial proof
term are seen as proof obligations, whose actual proofs are left to
the user. We show that the validity of those proof obligations
implies the total correctness of the program.
We also establish a result of partial completeness.
This work has been implemented in the Coq proof assistant.
It appears as a tactic taking an annotated program as argument and
generating a set of proof obligations. Several nontrivial
algorithms have been certified using this tactic.}
}
@ARTICLE{Filliatre99c,
author = {J.-C. Filli\^atre},
title = {{Formal Proof of a Program: Find}},
journal = {Science of Computer Programming},
year = 2006,
doi = {10.1016/j.scico.2006.10.002},
note = {To appear},
url = {http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz},
abstract = {In 1971, C.~A.~R.~Hoare gave the proof of correctness and termination of a
rather complex algorithm, in a paper entitled \emph{Proof of a
program: Find}. It is a hand-made proof, where the
program is given together with its formal specification and where
each step is fully
justified by a mathematical reasoning. We present here a formal
proof of the same program in the system Coq, using the
recent tactic of the system developed to establishing the total
correctness of
imperative programs. We follow Hoare's paper as close as
possible, keeping the same program and the same specification. We
show that we get exactly the same proof obligations, which are
proved in a straightforward way, following the original paper.
We also explain how more informal reasonings of Hoare's proof are
formalized in the system Coq.
This demonstrates the adequacy of the system Coq in the
process of certifying imperative programs.}
}
@TECHREPORT{Filliatre99b,
author = {J.-C. Filli\^atre},
title = {{A theory of monads parameterized by effects}},
institution = {{LRI, Universit\'e Paris Sud}},
type = {{Research Report}},
number = {1367},
month = {November},
year = 1999,
url = {http://www.lri.fr/~filliatr/ftp/publis/monads.ps.gz},
abstract = {Monads were introduced in computer science to express the semantics
of programs with computational effects, while type and effect
inference was introduced to mark out those effects.
In this article, we propose a combination of the notions of effects
and monads, where the monadic operators are parameterized by effects.
We establish some relationships between those generalized monads and
the classical ones.
Then we use a generalized monad to translate imperative programs
into purely functional ones. We establish the correctness of that
translation. This work has been put into practice in the Coq proof
assistant to establish the correctness of imperative programs.}
}
@PHDTHESIS{Filliatre99,
author = {J.-C. Filli\^atre},
title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
type = {Th{\`e}se de Doctorat},
school = {Universit\'e Paris-Sud},
year = 1999,
month = {July},
url = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
abstract = {Nous étudions le problème de la certification de programmes mêlant
traits impératifs et fonctionnels dans le cadre de la théorie des
types.
La théorie des types constitue un puissant langage de spécification,
naturellement adapté à la preuve de programmes purement
fonctionnels. Pour y certifier également des programmes impératifs,
nous commençons par exprimer leur sémantique de manière purement
fonctionnelle. Cette traduction repose sur une analyse statique des
effets de bord des programmes, et sur l'utilisation de la notion de
monade, notion que nous raffinons en l'associant à la notion d'effet
de manière générale. Nous montrons que cette traduction est
sémantiquement correcte.
Puis, à partir d'un programme annoté, nous construisons une preuve
de sa spécification, traduite de manière fonctionnelle. Cette preuve
est bâtie sur la traduction fonctionnelle précédemment
introduite. Elle est presque toujours incomplète, les parties
manquantes étant autant d'obligations de preuve qui seront laissées
à la charge de l'utilisateur. Nous montrons que la validité de ces
obligations entraîne la correction totale du programme.
Nous avons implanté notre travail dans l'assistant de preuve
Coq, avec lequel il est dès à présent distribué. Cette
implantation se présente sous la forme d'une tactique prenant en
argument un programme annoté et engendrant les obligations de
preuve. Plusieurs algorithmes non triviaux ont été certifiés à
l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
Knuth-Morris-Pratt).}
}
@INPROCEEDINGS{FilliatreMagaud99,
author = {J.-C. Filli\^atre and N. Magaud},
title = {{Certification of sorting algorithms in the system Coq}},
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 system Coq, 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://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}
}
@INPROCEEDINGS{Filliatre98,
author = {J.-C. Filli\^atre},
title = {{Proof of Imperative Programs in Type Theory}},
booktitle = {International Workshop, TYPES '98, Kloster Irsee, Germany},
publisher = {Springer-Verlag},
volume = 1657,
series = {Lecture Notes in Computer Science},
month = MAR,
year = {1998},
abstract = {We present a new approach to certifying imperative programs,
in the context of Type Theory.
The key is a functional translation of imperative programs, which is
made possible by an analysis of their effects.
On sequential imperative programs, we get the same proof
obligations as those given by Floyd-Hoare logic,
but our approach also includes functional constructions.
As a side-effect, we propose a way to eradicate the use of auxiliary
variables in specifications.
This work has been implemented in the Coq Proof Assistant and applied
on non-trivial examples.},
url = {http://www.lri.fr/~filliatr/ftp/publis/types98.ps.gz}
}
@TECHREPORT{Filliatre97,
author = {J.-C. Filli\^atre},
institution = {LIP - ENS Lyon},
number = {97--04},
title = {{Finite Automata Theory in Coq:
A constructive proof of Kleene's theorem}},
type = {Research Report},
month = {February},
year = {1997},
abstract = {We describe here a development in the system Coq
of a piece of Finite Automata Theory. The main result is the Kleene's
theorem, expressing that regular expressions and finite automata
define the same languages. From a constructive proof of this result,
we automatically obtain a functional program that compiles any
regular expression into a finite automata, which constitutes the main
part of the implementation of {\tt grep}-like programs. This
functional program is obtained by the automatic method of {\em
extraction} which removes the logical parts of the proof to keep only
its informative contents. Starting with an idea of what we would
have written in ML, we write the specification and do the proofs in
such a way that we obtain the expected program, which is therefore
efficient.},
url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR97/RR97-04.ps.Z}
}
@TECHREPORT{Filliatre95,
author = {J.-C. Filli\^atre},
institution = {LIP - ENS Lyon},
number = {96--25},
title = {{A decision procedure for Direct Predicate
Calculus: study and implementation in
the Coq system}},
type = {Research Report},
month = {February},
year = {1995},
abstract = {The paper of J. Ketonen and R. Weyhrauch \emph{A
decidable fragment of Predicate Calculus} defines a decidable
fragment of first-order predicate logic - Direct Predicate Calculus
- as the subset which is provable in Gentzen sequent calculus
without the contraction rule, and gives an effective decision
procedure for it. This report is a detailed study of this
procedure. We extend the decidability to non-prenex formulas. We
prove that the intuitionnistic fragment is still decidable, with a
refinement of the same procedure. An intuitionnistic version has
been implemented in the Coq system using a translation into
natural deduction.},
url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-25.ps.Z}
}
@TECHREPORT{Filliatre94,
author = {J.-C. Filli\^atre},
month = {Juillet},
institution = {Ecole Normale Sup\'erieure},
title = {{Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct~: \'etude et impl\'ementation dans le syst\`eme Coq}},
type = {Rapport de {DEA}},
year = {1994},
url = {ftp://ftp.lri.fr/LRI/articles/filliatr/memoire.dvi.gz}
}