Figure 2: Architecture of the HOL-CASL system
The Bremen HOL-CASL system consists of several parts, which are shown in Fig. 2. The parser checks the syntactic correctness of a specification (CASL Text) according to the CASL grammar and produces an abstract syntax tree (coded as ATerms). The static checker checks the static semantic correctness (according to the static semantics) and produces a global environment (also coded as ATerms) that associates specification names with specification-specific information such as the signature. The LaTeX formatter allows to pretty print CASL specifications (which are input in ASCII format), using the LaTeX package from Peter Mosses [Mos98].
Finally, the encoding is a bridge from CASL to first- or higher-order logic (FOL/HOL). It throws out subsorting and partiality by encoding it [MKK98], and thus allows to re-use existing theorem proving tools and term rewriting engines for CASL. Typical applications of a theorem prover in the context of CASL are
