Previous
Page

Applications 
Programming: One of the first application was to prototype the fundamental mechanisms of logic and functional programming languages like firstorder resolution and calculus. The general framework of Constraint Logic Programming can be easily designed in the ELAN framework [19], since its operational semantics is clearly formalised as rewrite rules, although the application strategy is often defined in an informal way. Some implementations [22] related to a calculus of explicit substitutions (the firstorder rewrite system that mimics calculus) open the way of implementing higherorder logic programming languages via a firstorder setting. Another calculus of explicit substitutions based on the calculus is used to provide a formal specification of Input/Output for ELAN [23].
Proving: ELAN was used in order to implement a predicate prover based on the rules proposed by J.R. Abrial, and implemented in the Btools . We developed also a propositional sequent calculus, completion procedures for rewrite systems [24]. A library for automata construction and manipulation has been designed. Approximation automata are used to check conditions for reachability, sufficient completeness, absence of conflicts in systems described by nonconditional rewrite rules [25].
Solving: The notion of rewriting controlled by strategies is used in [21] to describe in a unified way the constraint solving mechanism as well as the metalanguage needed to manipulate the constraints. This provides programs that are very close to the proof theoretical setting used now to describe constraint manipulations like unification or numerical constraint solving. ELAN offers a constraint programming environment where the formal description of a constraint solver is directly executable. ELAN has been tested on several examples of constraint solvers for various computation domains and combinations like abstract domains [21][27] (term algebras) and more concrete ones (booleans, integers, reals). In [28][29][30][31], it is shown how to use computational systems as a general framework for handling Constraint Satisfaction Problems (CSP for short). The approach leads to the design in ELAN of COLETTE, a solver for constraints over integers and finite domains.