Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Ergo is capable of generating proof traces for CC(X). Alternatively, Ergo can also be called interactively as a simple oracle without further verification. It is currently used to prove correctness of C and Java programs as part of the Why platform.

The problem of disjoint sets, also known as union-find, consists in maintaining a partition of a finite set within a data structure. This structure provides two operations: a function find returning the class of an element and a function union merging two classes. An optimal and imperative solution is known since 1975. 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 as efficient as its imperative counterpart. To achieve this result, our solution makes heavy use of imperative features and thus it is a significant example of a data structure whose side effects are safely hidden behind a persistent interface. To strengthen this last claim, we also detail a formalization using the Coq proof assistant which shows both the correctness of our solution and its observational persistence

We present a mechanism to automate equality proofs in skeptical proof assistants. The equality we consider is the combination of the pure theory of equality over uninterpreted symbols and a built-in decidable theory X. Our approach is intermediate between traditional complete proof reconstruction and verified provers. Reasoning about X is implemented independently in the proof assistant and as an external decision procedure. This double blind computation enables both tools to interact only by lightweight traces about pure equalities which are produced by the decision procedure and interpreted by the proof assistant. We validate our approach with the Coq proof assistant and our decision procedure CC(X), a congruence closure algorithm modulo a built-in theory. CC(X) is implemented as a module parameterized by X and the Coq development follows the same modular architecture. Currently, we have instantiated X by the theory of linear arithmetic.

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-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure. Additionally, we give some examples of semi-persistent data structures (arrays, lists and hash tables).

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and a union X of solvable theories. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak approach by the use of semantical values for class representatives instead of syntactical canonizers. This seemingly insignificant difference has strong impact on efficiency and expressiveness. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantical values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification.

This paper details the design and implementation of Ocamlgraph A highly 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. Algorithms are written independently from graph data structures, which allows combining user data structure (resp. algorithm) with Ocamlgraph algorithm (resp. data structure). Genericity is obtained through massive use of the Ocaml module system and its functions, the so-called functors.

Le problème des classes disjointes, connu sous le nom de union-find, consiste à maintenir dans une structure de données une partition d'un ensemble fini. Cette structure fournit deux opérations : une fonction find déterminant la classe d'un élément et une fonction 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 (backtracking). Nous présentons dans cet article une version persistante de 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.

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.

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.

If there exist efficient procedures (canonizers) for reducing terms of two first-order theories to canonical form, can one use them to construct such a procedure for terms of the disjoint union of the two theories? We prove this is possible whenever the original theories are convex. As an application, we prove that algorithms for solving equations in the two theories (solvers) cannot be combined in a similar fashion. These results are relevant to the widely used Shostak's method for combining decision procedures for theories. They provide the first rigorous answers to the questions about the possibility to directly combine canonizers and solvers.

Implementing efficient algorithms for combining decision procedures has been a challenge and their correctness precarious. In this paper we describe an inference system that has the classical Nelson-Oppen procedure at its core and includes several optimizations: variable abstraction with sharing, canonization of terms at the theory level, and Shostak's streamlined generation of new equalities for theories with solvers. The transitions of our system are fine-grained enough to model most of the mechanisms currently used in designing combination procedures. In particular, with a simple language of regular expressions we are able to describe several combination algorithms as strategies for our inference system, from the basic Nelson-Oppen to the very highly optimized one recently given by Shankar and Ruess. Presenting the basic system at a high level of generality and non-determinism allows transparent correctness proofs that can be extended in a modular fashion whenever a new feature is introduced in the system. Similarly, the correctness proof of any new strategy requires only minimal additional proof effort.

We present a framework to extend, in a modular way, the type systems of process calculi with information-flow annotations that ensure a noninterference property based on weak barbed bisimulation. Our method of adding security annotations readily supports modern typing features, such as polymorphism and type reconstruction, together with a noninterference proof. Furthermore, the new systems thus obtained can detect, for instance, information flow caused by contentions on distributed resources, which are not detected in a satisfactory way by using testing equivalences.

We present a generic constraint-based type system for the join-calculus. The key issue is type generalization, which, in the presence of concurrency, must be restricted. We first define a liberal generalization criterion, and prove it correct. Then, we find that it hinders type inference, and propose a cruder one, reminiscent of ML's value restriction. We establish type safety using a semi-syntactic technique, which we believe is of independent interest. It consists in interpreting typing judgements as (sets of) judgements in an underlying system, which itself is given a syntactic soundness proof. This hybrid approach allows giving pleasant logical meaning to high-level notions such as type variables, constraints and generalization, and clearly separating them from low-level aspects (substitution lemmas, etc.), which are dealt with in a simple, standard way.

This paper shows how to systematically extend an arbitrary type system with dependency information, and how the new system's soundness and non-interference proofs may rely upon, rather than duplicate, the original system's soundness proof. This allows enriching virtually any of the type systems known today with information flow analysis, while requiring only a minimal proof effort.

Our approach is based on an untyped operational semantics for a labelled calculus akin to core ML. Thus, it is simple, and should be applicable to other computing paradigms, such as object or process calculi.

The paper also discusses access control, and shows it may be viewed as entirely independent of information flow control. Letting the two mechanisms coexist, without interacting, yields a simple and expressive type system, which allows, in particular, ``selective'' declassification.

Jocaml is a system for mobile agents built inside the Objective-Caml language. Jocaml eases the development of concurrent, distributed and mobile agent based applications, by expressing useful distribution abstractions using a small set of simple but powerful primitives taken from the Join-Calculus[?].

The system provides total transparency for migration, application states (after migration, all threads resume their execution in the state before migration), communications (communication channels with other agents are kept during migration) and composition (sub-agents migrate with their parent agent). Other features of the Jocaml system are mobile objects with transparent remote method invocation, distributed garbage collection, failure detection and execution efficiency. Jocaml has already been used in several applications, such as a mobile editor, some distributed games and a distributed implementation of Ambients[?].

This paper describes the Jocaml programming model and language, its current implementation and some interesting applications.