10:15 Wed 4 June 1997

Ernest Teniente, Universitat Politecnica de Catalunya, Barcelona, Hiszpania: Deductive databases The goal of this seminar is to present deductive databases. Deductive databases generalize relational databases by including not only base facts and integrity constraints, but also deductive rules. Using these rules, new derived facts may be deduced from facts explicitly stored in the database. Integrity constraints are used for defining conditions that every state of the database should satisfy. Among other components, deductive databases include a query processing and an update processing system. The query processing system is aimed at providing the answer to the queries over base and derived predicates explicitly requested by the user. On the other hand, the update processing system provides the user with a uniform interface in which they can request different kind of updates, e.g. updates of base facts, updates of derived facts, updates of deductive rules and updates of integrity constraints. During the seminar, the main concepts of deductive databases will be presented and an special attention will be given to the problems encountered when querying and updating a database.

10:15 Wed 28 May 1997

Tomasz Borzyszkowski: System wnioskowania dla specyfikacji strukturalnych We srode 28.05.97 o 10:00 (zbiorka na UG w 115) chcialbym opowiedziec o szczegolach dowodu twierdzenia o zupelnosci systemu wnioskowania dla specyfikacji strukturalnych. Szczegoly dowodu oraz potrzebne definicje mozna znalezc w powstajacej pracy ``Correctness of the logical system for structured specifications''. Przyjemnej lektury :-)

10:15 Wed 14 May 1997

Andrzej Borzyszkowski: Teoria homotopii w pewnym dowodzie z dziedziny ,,rownoleglosc'' Transakcja nazywamy ciag wykonan akcji, ktory to ciag musi byc niepodzielny w jakims sensie. Akcje polegaja na czytaniu lub zapisie np. rekordow danych. Rownolegle wykonywanie wielu transakcji wymaga blokowania dostepu do rekordow przez transakcje, tak aby nie weszly sobie w droge. Najbezpieczniej by bylo, by transakcje byly wykonywane sekwencyjnie. Oczywiscie jest to nierealne z wielu powodow pragmatycznych. Bezpiecznym wykonaniem zbioru transakcji nazwiemy wykonanie rownowazne sekwencyjnemu, precyzyjna definicja rownowaznosci bedzie podana. Pytanie, w jaki sposob zagwarantowac bezpieczenstwo wykonywania transakcji. Twierdzenie (wyssane przez bazodanowcow z mlekiem matki): jesli wszystkie transakcje najpierw blokuja jakies rekordy a dopiero potem zwalniaja blokady (blokowanie dwufazowe), to ich zestaw bedzie obowiazkowo wykonany w sposob bezpieczny. Na seminarium podam dowod korzystajacy z teorii homotopii. Teorii tej nie trzeba sie bac, jest to tylko formalizm ulatwiajacy wyrazenie oczywistych intuicji geometrycznych. W szczegolnosci nie beda badane grupy homotopii czegokolwiek.

10:15 Wed 23 Apr 1997	Wiesiek Paw/lowski: Formalizm do prezentowania system/ow logicznych Pozwala on na jednolite uj/ecie stosunkowo szerokiej klasy logik cz/esto spotykanych w zastosowaniach informatycznych (teoria specyfikacji). Daje te/z mozliwo/s/c ich ,,strukturalnego konstruowania''. S/lowa kluczowe: (context) institutions, parchments.

10:15 Wed 2 Apr and 10:15 Wed 9 Apr 1997

Bogdan Wiszniewski: Testowanie strukturalne programow sekwencyjnych i rownoleglych Autor prezentuje nowe podejscie do testowania strukturalnego, polegajace na specyficznym polaczeniu analizy statycznej i dynamicznej w formie scenariuszy testowych. Podejscie to pozwala budowac skuteczne w praktyce narzedzia do testowania strukturalnego programow, mimo znanych ograniczen wynikajacych z nadmiernej liczby sciezek w przypadku obecnosci petli w programie czy nadmiaru stanow do analizy w przypadku akcji wykonywanych rownolegle przez kilka programow. Scenariusz testowy laczy pojecie danych testowych z pojeciem lokalnego stanu procesu i pozwala analizowac aplikacje rownolegle na trzech poziomach abstrakcji: dynamicznych stanow kodu binarnego, rejestrowanych w trakcie wykonywania sie danej aplikacji, wartosci zmiennych i warunkow, rejestrowanych na poziomie analizy jej kodu zrodlowego, oraz zdarzen komunikacyjnych, rejestrowanych na poziomie wykonywanych przez nia zadan. Zastosowanie nowej formy interpretacji symbolicznej kodu, oraz dynamicznie otwieranych okien testowych umozliwilo konstruowanie testow strukturalnych dla zlozonych aplikacji rownoleglych, ktorych zachowanie trudno przewidziec przed ich faktycznym wykonaniem. Dzieki uwzglednieniu istotnych cech implementacyjnych szeregu realistycznych klas programow uzytkowych stalo sie mozliwe znaczne zredukowanie objetosci konstruowanych testow. Opisuja to formalnie modele obliczen iterowanych i zdarzen komunikacyjnych zdefiniowane przez autora. Dynamicznie kreowane scenariusze testowe moga byc automatycznie implementowane w formie skryptow testowych. Skrypty te umozliwiaja deterministyczne odtwarzanie uprzednio zarejestrowanych zachowan programu, ktore po odtworzeniu moga zostac zmodyfikowane przez uzytkownika w celu generowania nowych scenariuszy. Dzieki zastosowaniu specjalnie zdefiniowanego modelu rownoleglych przeplywow sterowania wykorzystujacego technike obiektowa, mozliwa jest pelna animacja rejestrowanych zachowan programu na poziomie zdarzen komunikacyjnych. Model ten umozliwia rowniez badania symulacjne scenariuszy testowych w sytuacji gdy bezposrednia rejestracja zachowan binarnego kodu programu jest zbyt czaso- lub pamiecio-chlonna. Prezentowane rozwiazania zostana zilustrowane przykladami uzycia narzedzi do testowania strukturalnego programow, ktore implementuja idee zaprezentowane przez autora. W szczegolnosci zaprezentowane zostanie narzedzie STEPS, zrealizowane dla projektu Copernicus. Umozliwia ono interakcyjna generacje scenariuszy testowych dla programow rownoleglych wykorzystujacych platforme PVM.

10:15 Wed 26 Mar 1997	Rafal Somla: Overview of Unification Theory (continued) At our next meeting I will continue presenting overview of Unification in nonempty theories. I will start with listing known results for various unification problems. Then I'm going to present some unification algorithms, and finally, the almost linear algorithm for standard unification (in empty theory).

10:15 Wed 19 Mar 1997	Stefan Sokolowski: Optymality of Hindley-Milner type inference Hindley-Milner algorithm uses unification (in an empty theory) to infer optimal (i.e. the most general) types for given expressions. The formal proof of this optimality is, however, a bit complicated. I am going to present the proof with a small flaw, which, I hope, the audience will help me to fix.

10:15 Wed 5 Mar 1997

Rafal Somla: Overview of Unification Theory I am going to report an article by F.Bader and J.H.Siekmann concerning the unification theory. I will introduce basic definitions and notions needed to state the so called E-unification problems. I will present main differences between E-unification and ordinary unification, and also I will list results for various E-unification problems. I'm afraid this time I won't be able to present any unification algorithms -- I didn't have enough time to prepare for this.

10:15 Wed 29 Jan 1997

Rafal Somla: Another approach to TFU problem On His last meeting Marek has shown, how PL_sigma can be used to specify actions and to express AI questions. As an example He used simple Turkey-Fred-Uzi problem. Using this example, I want to present a different approach, which is more semantic-based. I will use ideas found in Lamport's TLA logic and those, which I have presented during my speech about process specification last year.

9:15 Thu 23 Jan 1997

Pawel Paczkowski: Characterizing bisimilarity of value-passing parameterized processes Bisimulation is an equivlence relation that is widely used in various process algebras. In this talk I will demonstrate that showing (strong early) bisimulation equivalence can be reduced to finding a solution of a set of equations involving formulas of first order logic, when processes are represented as symbolic transition graphs extended with assignments. The talk is based on my paper ``Characterizing bisimilarity of value-passing parameterized processes'' presented at an INFINITY workshop.

10:00 Wed 15 Jan 1997

Marek Bednarczyk: AI applications of PL_sigma The logic of predicates with explicit substituitons, i.e., PL_sigma, has been used as a logic of specifications. This is a Computer Science application, in which formulae of PL_sigma are used to describe the meaning of programs. I plan to argue that it can be equally well applied in Artificial Inteligence, and for a similar purpose: specification of actions.

10:00 Wed 18 Dec 1996

Stefan Sokolowski: Hindley-Milner's term typing algorithm I am going to produce an algorithm that, given a term t and a context G, yields a type tp and a unifier s such that tp=tp s, prove its correctness: G s |- t : tp is derivable, prove its optimality: if G s' |- t : tp' s' is derivable then tp is more general than tp' and s is smaller than s'. I assume you know about unification (cf. ``Biala Ksiega unifikacji i typowania'').

14:00 Fri 13 Dec 1996	Didier Galmiche, UHP & IUF & CRIN-CNRS, Francja: Proofs, concurrent objects and computations in a Full Intuitionistic Linear Logic framework O modelowaniu obliczen przy pomocy logiki. Prezentowane podejscie okreslic mozna haslem: "Obliczenia jako Dowody". Dominique Mery, UHP & IUF & CRIN-CNRS, Francja: Temporal Abstract Machines O specyfikowaniu systemow reaktywnych dzialajacych w srodowiskach gwarantujacych rozmaite warianty "fairness".

10:00 Wed 4 Dec 1996	Marek Bednarczyk: pLSD versus B B comprises: a method (B-method), a logic (B-logic) and software support (B-tool, atelierB) for the rigorous development of software from specifications. The B method is based on weakest precondition predicate transformers. During the talk I plan to give the evidence to support the hypothesis, that B is closely related to pLSD.

9:00 Thu 28 Nov 1996

Ryszard Kubiak: On the nature of objects of polymorphic types From the mere polymorphic type of an object one can deduce the properties of that object. This was discovered by Reynolds and then popularized by Wadler in his paper ,,Theorems for Free!''. For example, let 'X' be a closed type term (in system F) and consider the polymorphic type 'forall a. (X->a)->a'. Using the ,,Theorems for Free'' methodology one can prove that the type is isomorphic to 'X'. More precisely, the meanings of those types in appropriately chosen models are isomorphic. Using the same approach one can prove that there are no terms of the polymorphic type 'forall a. X->a'. By showing how the methodology works on simple examples I am going to prepare the listeners for more advanced cases to be demonstrated in the near future.

10:00 Wed 20 Nov 1996

Stefan Sokolowski: Unification in context Unification is a method for solving syntactic equations. It is used in virtually any type checker to guess implicit types. The idea is to find the most general substitution of types for type variables that would make two syntactic types equal. In the case of types depending on individual variables, the well-formedness and the meaning of types substituted may critically depend on the context in which the variables are introduced. In that case, the unification becomes much more involved. I will try to introduce the problem and to suggest a due theorem, but I do not yet know the details. I count on a feedback from the audience.

9:00 Thu 14 Nov 1996

Barbara Morawska: Izomorfizm Curry-Howarda Na poczatek przypomne reguly naturalnej dedukcji, potem krotko rachunek lambda z typami, nastepnie na czym polega normalizacja dowodow naturalnej dedukcji i jak dokladnie odpowiada jej normalizacja termow. Wtedy krotko przedstawie rachunek sekwentow i w jaki sposob kazdej "naturalnej dedukcji" odpowiada dedukcja sekwentow (ale nie ma tu izomorfizmu). W koncu mam zamiar pokazac dlaczego eliminacja ciecia jest tym samym co normalizacja dowodow.

9:00 Thu 7 Nov 1996

Tomasz Borzyszkowski: From EML specifications to SML programs The original methodology was presented in: ``Formal program development in Extended ML for the working programmer'' written by Donald Sannella. Abstract (from the paper): Extended ML is a framework for the formal development of programs in Standard ML programming language from high-level specifications of their required input/output behaviour. It strongly supports the development of modular programs consisting of an interconnected collection of generic and reusable units. The Extended ML (EML) framework includes a methodology for formal program development which establishes a number of ways of proceeding from a given specification of a programming task towards a program. Each such step gives rise to one or more proof obligations which must be proved in order to establish the corretness of that step. This paper is intended as a user-oriented summary of EML language and methodology. Theoretical technicalities are avoided whenever possible, with emphasis placed on the practical aspects of formal program development. An extended example of a complete program development in EML is included.

9:00 Thu 31 Oct 1996

Marek Bednarczyk: Modular Programming & Implication Higher-order programming was a central issue of the GDM Project, see e.g. ``Partial correctness -- the single assertion approach'' (a collection of reports,ed. Stefan Sokolowski). I plan to give an explanation of program modules as "proofs" of the formal implication of the programming logic pLSD based on the analogy with the Curry-Howard isomorphism between lambda-abstractions and proofs of implications.

9:00 Thu 24 Oct 1996

Stefan Sokolowski: Intersection types in subset type reconstruction Subset type reconstruction is the assignment of types of the form (x:tp1|F)->tp2 to terms; the notation stands for ``the set of functions which, given an x from tp1 for which F holds, yield a result in tp2''. In some cases, a natural candidate for a reconstructed type of a functional term is the intersection of a family of types. I would like you to help me to come up with appropriate requirements on the language for formulae F, under which such intersection would be expressible. This is important for the design and verification using deductive systems but please, let us not discuss the relation during the meeting.