Static semantic analysis and theorem proving for CASL

Abstract

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 axe 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.