Executing CASL Equational Specifications with the ELAN Rewrite Engine

Hélène Kirchner
Christophe Ringeissen1

October 22, 1999

This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.3.

Abstract

We define in this note the class of CASL programs executable with the ELAN system, that performs efficient rewriting modulo associativity-commutativity. We describe the technique used to translate CASL equational specifications into ELAN rewrite programs and to execute them.
  • 1 Introduction
  • 2 ELAN Programs
  • 3 Mapping from CASL to ELAN
  • 4 ATerm-instances for CASL and ELAN
  • 5 Available Tools for Executing CASL Equational Specifications
  • 6 A Complete Simple Example
  • 7 Further Developments
  • Acknowledgements
  • References
  • Footnotes
    • CoFI Note: T-9 -- Version:  -- October 22, 1999.
    Comments to Christophe.Ringeissen@loria.fr