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.