### Abstract

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.

Original language | English |
---|---|

Title of host publication | Proceedings of WADT'99 |

Publication date | 1999 |

Pages | 30-31 |

Publication status | Published - 1999 |

Event | 14th Int. Workshop on Algebraic Development Techniques - Bonas Duration: 1 Jan 1999 → … |

### Conference

Conference | 14th Int. Workshop on Algebraic Development Techniques |
---|---|

City | Bonas |

Period | 01/01/1999 → … |

## Cite this

Haxthausen, A., Mossakowski, T., & Krieg-Bruckner, B. (1999). Subsorted Partial Higher-order Logic as an Extension of CASL. In

*Proceedings of WADT'99*(pp. 30-31)