The are quite a number of existing specifications languages and tools for them. CASL was designed with the goal of providing a common language for better tool interoperability. This is reflected by having a common interchange format for CASL tools, the ATerm format [BJKO99, vdBKO98]. ATerms are an easy-to-handle format with libraries in several languages (C, Java, ML) available. They are used as low level tool format for data exchange between CASL tools. Based on this format, several formats have been designed: the CasFix format [vdB98] for abstract syntax trees, and a format for the global environment, containing the static semantic information.
By providing conversions from and to ATerms at all intermediate points in the tool architecture, the Bremen HOL-CASL system can be used as a front-end or back-end in combination with other tools. Actually, it has been combined as a back-end with the Amsterdam CASL parser [vdBS99], and as a front-end with several theorem proving tools: ELAN [KR99], PVS [Bai99] and Isabelle (see section 7). See also the CoFI Tools Group home page [CoFb].