*
About congruence-closure in the Coq proof assistant
*

Master's thesis, University Paris 7, September 2001 (in french) : ps

*
Automated reasoning in Type Theory
*

PhD thesis , University Paris 11, september 2005 (in french) : ps.gz, pdf

Research Report 1380, LRI, December 2003 : ps

In this report we present a contraction-free sequent calculus
including inductive
definitions for the first-order intuitionistic logic. We show that it
is a natural extension to Dyckhoff's *LJT* calculus and we prove the
contraction- and cut-elimination properties, thus extending
Dyckhoff's result, in order to validate its use as a basis for
proof-search procedures. Finally we describe the proof-search
strategy used in our implementation as a tactic in the Coq
proof assistant.

in TYPES 2003 : Types for Proofs and Programs, LNCS 3085 , pages 162-177.

© 2004 Springer-Verlag : ps

*
Short version of the above
*

*
Skip lists and probabilistic binary search trees
*

in Seizièmes Journées Francophones des Langages Applicatifs.

© 2005 INRIA (in french) : ps

In 1989, William Pugh published a paper whose title was
*Skip lists: a probabilistic alternative to binary trees* in
which he analyzed in detail the performance of a mutable data
structure named *skip-list*. This data structure represents
ordered finite sets by lists with levels, each element having a
randomly-assigned level. In this paper we describe how our attempt to
implement these levelled lists as a persistent datastructure in
Objective Caml allowed to identify a strong relationship between this
data structure and random binary trees.

in 20th International Conference on Automated Deduction,
LNAI 3632, pages 7-22.

© 2005 Springer-Verlag : ps,
pdf

Our general goal is to provide better automation in interactive proof assistants such as Coq. We present an interpreter of proof traces in first-order multi-sorted logic with equality. Thanks to the reflection ability of Coq, this interpreter is both implemented and formally proved sound --- with respect to a reflective interpretation of formulae as Coq properties --- inside Coq's type theory. Our generic framework allows to interpret proofs traces computed by any automated theorem prover, as long as they are precise enough: we illustrate that on traces produced by the CiME tool when solving unifiability problems by ordered completion. We discuss some benchmark results obtained on the TPTP library.

in TYPES 2006: Types for Proofs and Programs, LNCS 4502, pages 78-92.

© 2007 Springer-Verlag : pdf

We give a decision procedure for the satisfiability of finite sets of
ground equations and disequations in the *constructor theory*: the
terms used may contain both uninterpreted and constructor function
symbols. Constructor function symbols are by definition injective
and terms built with distinct constructors are themselves distinct.
This corresponds to properties of (co-)inductive type constructors
in inductive type theory. We do this in a framework where function
symbols can be partially applied and equations between functions are
allowed. We describe our algorithm as an extension of
*congruence-closure* and give correctness, completeness and
termination arguments. We then proceed to discuss its limits and
extension possibilities by describing its implementation in the Coq
proof assistant.

in Towards Mechanized Mathematical Assistants

14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, proceedings, LNCS 4573, pages 78-92.

© 2007 Springer-Verlag : pdf

We present a new framework for the online development of formalized mathematics. This framework allows wiki-style collaboration while providing users with a rendered and browsable version of their work. We describe a prototype based on Coq, its web interface as implemented by the second author, and a modified version of the MediaWiki code-base. We discuss open issues such as dependencies and repository consistency. We explain limitations of the current prototype and we give a perspective towards a more robust solution.

This work was funded by NWO Bricks/Focus Project 642.000.501 (Advancing the Real use of Proof Assistants) and partially funded by NWO FEAR Project

in TYPES 2007 : Types for Proofs and Programs, LNCS 4941.

© 2008 Springer-Verlag : pdf

Also in Theorem Proving in
Higher-Order Logics : Emerging Trends Proceedings

Technical report 364/07, Computer Science Department,
University of Kaiserslautern

This paper presents a new proof language for the Coq proof assistant. This language uses the declarative style. It aims at providing a simple, natural and robust alternative to the existing Ltac tactic lan- guage. We give the syntax of our language, an informal description of its commands and its operational semantics. We explain how this language can be used to implement formal proof sketches. Finally, we present some extra features we wish to implement in the future.

Poster - Bricks midterm Symposium ps.gz (A3) pdf

in Proceedings of the 3rd Semantic Wiki Workshop

SemWiki 2008 -- The Wiki Way of Semantics :
SALTed PDF

Abstract. Mathematical documents, and their instrumentation by computers, have rich structure at the layers of presentation, metadata and semantics, as objects in a system for formal mathematical logic. Semantic Web tools support the first two of these, with little, if any, contribution to the third, while Proof Assistants instrument the third layer, typically with bespoke approaches to the first two. Our position is that a web of mathematical documents, definitions and proofs should be given a fully-fledged semantics in terms of the third layer. We propose a "MathWiki" to harness Web 2.0 tools and techniques to the rich semantics furnished by contemporary Proof Assistants.