Subsorted Partial Higher-order Logic as an extension of CASL

CASL is a specification language combining first-order logic, partiality and subsorting. However, inmany applications, first-order logic does not suffice. Consider e.g. the specification of functionalprograms, which often gain their conciseness through the use of higher-order functions, or thespecification of predicate transformers, which is inherently higher-order. This work generalizes the CASL logic to also include higher-order functions and predicates. Thecombination of subsorting, partiality, higher-order functions and predicate logic is new to ourknowledge. The logic is presented in a modular step-by-step reduction: the logic is defined in terms of a generalizedsubsorted partial logic which in turn is defined in terms of many-sorted partial first-order logic. Webelieve that it is crucial to follow this modular style for two main reasons. One reason is reduction ofcomplexity. We use a two step reduction involving three logics in our presentation, adding new featuresstep by step. Thus each step (and its interaction with the previous steps) can be understood separately.This is important since there is quite a number of different non-trivial interactions. The other reason iscompatibility of sublanguages and extensions. First of all, (first-order) CASL should be faithfullyembeddable into its higher-order extension. Secondly, it should be possible easily to restricthigher-order CASL to various sublanguages, as it has been done for first-order CASL. A new notion of homomorphism is introduced to meet the need to get a faithful embedding offirst-order CASL into higher-order CASL. Finally, it is discussed how a proof calculus for the proposedlogic can be developed.