With respect to the work presented at WADT'99, we have significantly extended the class of CASL specifications that can be executed with ELAN. It is now possible to consider structured CASL specifications and CASL mixfix signatures, including predicates.
Beyond these rather easy extensions, some challenging questions still remain: for instance, how to integrate ELAN labelled rules and strategies into CASL? How to deal with the specification of non-deterministic functions in CASL? In ELAN, non determinism is allowed since a computation can have a multiset of results (i.e. of normal forms). We could describe such specifications by introducing multiset operations to handle multisets of results, as done for instance in [Bor98]. In this case of course, execution of specifications with associative and commutative functions (like multiset union) is of prime interest.