This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.
This paper presents a static semantic analysis for CASL, the Common Algebraic Specification Language. Abstract syntax trees are generated including subsorts and overloaded functions and predicates. The static semantic analysis, through the implementation of an overload resolution algorithm, checks and qualifies these abstract syntax trees. The result is a fully qualified CASL abstract syntax tree where the overloading has been resolved. This abstract syntax tree corresponds to a theory in the institution underlying CASL, subsorted partial first-order logic (SubPFOL).Two ways of embedding SubPFOL in higher-order logic (HOL) of the logical framework Isabelle are discussed: the first one from SubPFOL to HOL via PFOL (partial first-order logic) first drops subsorting and then partiality, and the second one is the counterpart via SubFOL (subsorted first-order logic). Finally, we sketch an integration of the embedding of CASL into the UniForM Workbench.
This document has been revised and published [MKKB98]. The original version is no longer available, and future citations should refer to the published version, which is available by FTP.