Constructs and Features]: Data types and structures General Terms Algorithms, Data Structures (2009)
This functional pearl proposes an ML implementation of the Garsia–Wachs algorithm. This somewhat obscure algorithm builds a binary tree with minimum weighted path length from weighted leaf nodes...
Formal Verification of MIX Programs (2008)
We introduce a methodology to formally verify MIX programs. It consists in annotating a MIX program with logical annotations and then to turn it into a set of purely sequential programs on which...
Optimal Solution: Tarjan’s Algorithm (2008)
Sylvain Conchon, Jean-christophe Filliâtre, Sylvain Conchon, Jean-christophe Filliâtre
goal: a data structure to maintain a partition of {0, 1,..., n − 1} imperative data structure: module type ImperativeUnionFind = sig type t val create: int → t val find: t → int → int val...
Formal Verification of MIX Programs (2008)
We introduce a methodology to formally verify MIX programs. It consists in annotating a MIX program with logical annotations and then to turn it into a set of purely sequential programs on which...
Gagner en passant à la corde (2008)
Cet article présente une réalisation en OCaml de la structure de cordes introduite par Boehm, Atkinson et Plass. Nous montrons notamment comment cette structure de données s'écrit naturellement...
Gagner en passant à la corde (2008)
Cet article présente une réalisation en OCaml de la structure de cordes introduite par Boehm, Atkinson et Plass. Nous montrons notamment comment cette structure de données s'écrit naturellement...
Certification of Sorting Algorithms in the Coq System (2007)
Jean-Christophe Filliâtre, Nicolas Magaud
We present the formal proofs of total correctness of three sorting algorithms in the Coq proof assistant, namely insertion sort, quicksort and heapsort. The implementations are imperative programs...
Verification of Non-Functional Programs using Interpretations in Type Theory (2007)
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...
ICS: Integrated Canonizer and Solver (Tool Presentation) (2007)
Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, N. Shankar
ver linear arithmetic terms and propositional logic [1]. The theory currently includes: The usual propositional constants true, false and connectives not, &, |, =>, <=>. Equality (=) and...
The Why/Krakatoa/Caduceus platform for deductive program verification (2007)
Filliâtre, Jean-Christophe, Marché, Claude
We present the Why/Krakatoa/Caduceus set of tools for deductive verification of Java and C source code.
The Why/Krakatoa/Caduceus platform for deductive program verification (2007)
Filliâtre, Jean-Christophe, Marché, Claude
We present the Why/Krakatoa/Caduceus set of tools for deductive verification of Java and C source code.
Semi-Persistent Data Structures (2007)
Sylvain Conchon, Jean-christophe Filliâtre
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called...
Semi-Persistent Data Structures (2007)
Sylvain Conchon, Jean-christophe Filliâtre
Abstract. A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called...
Filliatre J C, Paris Sud, Jean-christophe Filliâtre
Iterating over the elements of an abstract collection is usually done in ML using a higher-order function provided by the data structure. This article introduces a new paradigm of iteration, using...
Functors for Proofs and Programs (2004)
Filliâtre, Jean-Christophe, Letouzey, Pierre
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...
Functors for Proofs and Programs (2004)
Filliâtre, Jean-Christophe, Letouzey, Pierre
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...
Formal Proof of a Program: Find (2000)
In 1971, C. A. R. Hoare gave the proof of correctness and termination of a rather complex algorithm, in a paper entitled Proof of a program: Find. It is a hand-made proof, where the program is given...
A Theory of Monads Parameterized By Effects (1999)
Monads were introduced in computer science to express the semantics of programs with computational effects, while type and e ect inference was introduced to mark out those effects. In this article,...
Proof of Imperative Programs in Type Theory (1998)
We present a new approach to certifying functional programs with imperative aspects, in the context of Type Theory. The key is a functional translation of imperative programs, based on a combination...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
Proof of Imperative Programs in Type Theory (1997)
Ecole Normale, Suprieure Lyon, Jean-Christophe Filliâtre, Jean-christophe Filliatre
Proofs of correctness of imperative programs are traditionally done in first order frameworks derived from Hoare logic [8]. On the other hand, correctness proofs of purely functional programs are...
Finite Automata Theory in Coq - A constructive proof of Kleene's theorem (1997)
Ecole Normale, Suprieure Lyon, Jean-Christophe Filliâtre
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...
The Coq Proof Assistant, Reference Manual, Version 5.10 (1995)
Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Huet, Gerard, Manoury, Pascal, Munoz, César, ...
Résumé disponible dans les fichiers attachés
The Coq Proof Assistant, Reference Manual, Version 5.10 (1995)
Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Huet, Gerard, Manoury, Pascal, Munoz, César, ...
Résumé disponible dans les fichiers attachés
The Coq Proof Assistant - Reference Manual V 5.10 (1995)
Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Gérard Huet, Chetan Murthy, César Muñoz, ...
ion All Axiom Begin Cd Chapter Check CheckGuard CoFixpoint Compute Defined Definition Drop Elimination End Eval Explain Extraction Fact Fixpoint Focus for Go Goal Hint Hypothesis Immediate Induction...