EXTRA-Treffen Archiv Sommersemester 1997

10., 14., 16. Juli

        PRIESTLEY DUALITY AND PROGRAM SEMANTICS
        (3 Termine mit Diskussion und Ausrichtung auf Inhalte bzgl.
         des UniForM-Kontextes:
         Logics, Semantics and Combination of Methods)

        Prof. Dr. Chris Brink, University of Cape Town

        From non-classical logics we have the following paradigm: any
        well-behaved logic characterises and is characterised by both
        a relational structure (its Kripke semantics) and an algebra
        (its Lindenbaum-Tarski algebra -- typically some kind of lattice).
        Since programs can be regarded as binary relations over some
        state space, and hence as forming a relational structure, this
        raises the question whether the triangular relationship of
        logic-algebra-semantics also holds good for program semantics.
        The short answer is Yes. The long answer is that there is
        in fact a much richer relationship between four versions of
        program semantics: the relational model, predicate transformer
        semantics, information systems and powerdomains. We present the
        state space as a certain kind of Priestley space, and programs
        as certain structure-preserving relations over such a space. The
        technique of Priestley duality then allows a circular derivation
        of a predicate transformer semantics from the relational model,
        an information system from the predicate transformer semantics,
        a powerdomain from the information system, and the original
        relational model back again from the powerdomain. The information
        system is also related to Hoare logic. To clarify the intuition
        behind this approach we present a case study, which is a
        "Priestley version" of the so-called universal domain due to
        Plotkin. Various ideas about properties of programs and predicates
        can be explicated in terms of this case study.


13., 20., 27. Juni

        Eine Führung durch die wunderbare Welt der Kategorien.

        Christoph Lueth

        Kategorientheorie hat sich in den letzten fünfzehn Jahren als eines
        der wichtigsten mathematischen Hilfsmittel für theoretische und
        theoretisch orientierte Informatiker etabliert. Einige Konferenzen,
        wie z.B. LICS, sind ohne Grundkenntnisse in diesem Bereich mehr oder
        weniger unverständlich, und immer öfter gelten Grundkenntnisse in
        Kategorientheorie als unerläßlich.

        Ich werde versuchen, in drei Vorträgen eine Einführung in die
        Grundbegriffe der Kategorientheorie zu geben, und in einige Gebiete,
        von denen ich denke, daß sie für den praktisch arbeitenden
        theoretischen Informatiker (viz. uns) wichtig und interessant
        sind. Der Stil der Vorträge wird informell sein; ich werde versuchen,
        die grundlegenden Ideen darzustellen, ohne die (manchmal durchaus
        verwirrenden) technischen Details auszubreiten. Der Sinn der Übung ist
        zu zeigen, was man mit Kategorien alles machen kann, und ein paar
        Grundideen anzureißen. Die schweißtreibenden Einzelheiten überlasse
        ich dann gerne dem geneigten Zuhörer :-)



        Teil I:  Grundbegriffe
            - Kategorien, Funktoren und natürliche Transformationen
            - Funktorkategorien
            - Repräsentierbarkeit und das Yoneda-Lemma
            - Limiten, Kolimiten, Adjunktionen
            - Monaden
            - Monoidale und geschlossene Kategorien


        Teil II:  Monaden
            - Algebren für Monaden, die Eilenberg-Moore-Kategorie
            - die Kleisli-Konstruktion
            - Beck's Theorem und Monadizität
            - Universelle Algebra ist die Theorie von Monaden auf der
                Kategorie aller Mengen
            - Sketche, Lawvere-Theorien und die Gabriel-Ulmer-Dualität
            - Monaden als Fixpunkte: freie Monaden
            - Moggi's "computational monads"

        Teil III: Kategorielle Logik und Domaintheorie:
            -  Kartesisch geschlosssene Kategorien (ccc's) als Modelle für
               getypten Lambda-Kalküle; der getypte Lambda-Kalkül als interne
               Sprache von ccc's.
            -  Logik höherer Stufe in einem Topos
            -  Die kategorielle Lösung von Domain-Gleichungen


6.Juni  A Modular extension to Z for Specification, Reasoning and Refinement

        Owen Traynor, Software Verification Research Centre,
                The University of Queensland, Australia

        We introduce the concept of modules for the Cogito
        specification language, Sum (a variant of Z). An outline of the
        module reference mechanism, parameterisation and access methods is
        presented.  Some illustrative examples and rationale are included and
        the advantages of the module concept in the context of reasoning and
        refining (Z) specifications are discussed.

        Extensive tools support for the management and analysis of Sum
        specifications is available. A summary of these tools is given,
        together with an overview of the environment that has been
        constructed to allow reasoning about Sum specifications
        (i.e. to allow formal proof about properties of specifications).
        An outline of the tools available for animating Sum specifications and
        refining these specifications to Ada code is also given.

        A demonstration of the Cogito system will be given after the talk.


23.Mai        Static and Semantic Analysis of CASL

        Kolyang   B. Krieg-Brückner T. Mossakowski

        This talk presents a static and semantic analysis
        of CASL. Represented in the higher-order logical
        framework of Isabelle, the embedding yields abstract
        syntax trees, that are readed for a static-semantic check.
        Furthermore, an overload resolution algorithm is implemented
        that takes the resulting abstract trees and yields CASL fully
        qualified abstract trees.

        At the end, a schematic overall architecture of the embedding
        of CASL in a logical framework, using thus all facilities given by
        a generic theorem prover, is presented.


2.Mai   Bericht TAPSOFT'97

        Burkhart Wolff, Christoph Lüth


4.April
        Component Software Engineering in Object Orientation

        Prof. Dr. Yulin Feng, Academia Sinica, Peking

        The development of object oriented technology causes
        great changes to traditional methods of application software
        design. These changes make it possible that
        application systems can be constructed through some software
        components. It is not simply a set of prepackaged solutions
        from which a customer may pick and choose, it involves an
        actual custom tailoring and reengineering during the later
        1990's mass customization. The talk gives a brief
        description of our research on component software engineering
        in object orientation, including semantic model, specification
        languages, design methodology and OO trends and directions etc.