Subsorted Partial Higher-order Logic as an extension of CASL

T. Mossakowski, Anne Elisabeth Haxthausen, B. Krieg-Brückner

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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 languageEnglish
    Title of host publicationWADT'99
    PublisherSpringer Verlag
    Publication date2000
    Pages126-145
    Publication statusPublished - 2000
    Event14th International Workshop on Recent Trends in Algebraic Development Techniques - Château de Bonas, France
    Duration: 15 Sep 199918 Sep 1999
    Conference number: 14

    Workshop

    Workshop14th International Workshop on Recent Trends in Algebraic Development Techniques
    Number14
    CountryFrance
    CityChâteau de Bonas
    Period15/09/199918/09/1999

    Fingerprint Dive into the research topics of 'Subsorted Partial Higher-order Logic as an extension of CASL'. Together they form a unique fingerprint.

    Cite this