Standard ML (SML) is a functional programming language, equipped with a powerful module system. Extended ML (EML) is a framework for the formal development of programs in SML. As a language EML is an extension of (a large subset of) SML. The EML Kit is an implementation of the Extended ML programming language, developed by Marcin Jurdzinski, Mikolaj Konarski, Slawomir Leszczynski and Aleksy Schubert. After a short overview of the EML Kit, I will describe one of the problems, that arose during the work on the implementation of the EML language. The problem is type-checking of EML signatures in the presence of axioms. I will show how the most straightforward formulation of the task leads to the undecidability, explain the correct solution and comment on the algorithm that is used in its implementation in the EML Kit.
There are two widely accepted notions of behavioural equivalence, formalizing the idea of observational indistinguishability: observational equivalence for algebras and bisimulation equivalence (bisimilarity) for concurrent or nondeterministic processes. I will present an attempt to find some links between the two notions. I will show that the observational equivalences for standard, partial and regular algebras are bisimulation equivalences in the setting of open maps, proposed as an abstract approach to behavioural equivalences of processes. Open maps enable a uniform definition of behavioural equivalences across a range of different models for parallel computations, thus the main advantage of our results is capturing the models for sequential and concurrent systems in this uniform framework. In such an abstract setting I will formulate the property of determinism, shared by all the algebras considered, and identify some interesting facts satisfied by bisimilarity in a deterministic case. All the results for the algebras are obtained by the application of general theorems, stating that open maps are transported via adjunction and multiadjunction.
(Nie odbylo sie, zostanie przeniesione na pierwszy wolny termin.)
Na seminarium zamierzam wprowadzic ogolne zalozenia dotyczace powstajacego jezyka. Szczegolny nacisk zamierzam polozyc na dziedziczenie oraz zwiazane z nim pseudo-zmienne self i super. Algebra wyrazen zostanie ograiczona do niezbednego minimum.
Na seminarium przedstawie pewne stale punkty wszystkich kursow ,,Wstepu do matematyki'', t.j. zagadnienia zwiazane z rownaniami typu x=f(x). Zaprezentuje struktury algebraiczne, w ktorych rownania takie daja sie rozwiazac, dzieki czemu sa wykorzystywane do rekurencyjnego definiowania obiektow skladniowych i semantycznych. Pokaze tez sytuacje, w ktorych rownanie nie ma rozwiazania i opowiem, jak z nich wybrnac.
Na poprzednich seminariach przedstawiona zostala teoria rownan dziedzinowych na zbiorach lancuchowo zupelnych stosowanych w semantyce denotacyjnej. Problemy pojawiaja sie, gdy chcemy opisac np. jezyk, w ktorym procedura moze przyjac jako parametr dowolna procedure, czyli - ogolniej - pojawiaja sie rownania dziedzinowe typu D -> A + [ D -> D ]. Problem ten rozwiazal Dana Scott w latach 70'tych podajac konstrukcje modelu, w ktorym rownania tego typu maja rozwiazania.
W referacie omowie prace "DOMAINS FOR DENOTATIONAL SEMANTICS" Dana S. Scott '82. W pracy tej autor podaje kolejna propozycje matematycznego modelu, w ktorym to modelu mozna by definiowac w ulobiony juz przez nas sposob semantyki. Mianowicie wprowadzone zostaje pojecie (i odpowiednia kategoria) systemu informacyjnego (ang. information system). Jak sie zapewne przekonamy, wraz z nowym podejsciem pojawiaja sie nowe zalety...
W referacie pokaze rownowaznosc semantyk operacyjnej i denotacyjnej na przykladzie prostego jezyka while-programow. Zasadnicza wlasnoscia, ktora odroznia obie semantyki jest funkcja wartosciujaca, ktora w przypadku semantyki operacyjnej jest funkcja czesciowa, w semantyce denotacyjnej zas - zwykla funkcja lub "pinezka". Rownowaznosc obu semantyk sprowadza sie wiec do pokazania odpowiedniosci miedzy wyliczeniami skonczonymi oraz rownowaznosci miedzy brakiem wyliczenia w semantyce operacyjnej i "pinezka" w semantyce denotacyjnej.
(nie odbylo sie)
Dotychczas prezentowane dziedziny semantyczne D byly czesciowymi porzadkami , zas programy odpowiadaly funkcjom f: D -> D ( morfizmom) miedzy dziedzinami. To znaczy jezeli program wystartowal w stanie x z dziedziny D i
W swym wystapieniu bede rozwazal niedeterministyczne programy. Zaprezentuje rozne semantyki takich programow. W drugiej czesci pokaze, ze nie istnieje kompozycjonalna w sposob ciagly, stalopunktowa semantyka programow, w ktorych sa instrukcje niedeterministyczne, gdzie mozliwe jest przeliczalnie wiele wyborow. Jesli czas pozwoli, to przedstawie Hoare'owski system dowodowy dla while-programow z dodatkowa instrukcja niedeterministycznego przypisania: x := ? znaczy, ze x otrzymuje dowolna wartosc z dziedziny. Okazuje sie, ze jesli ta dziedzina jest przeliczalna, to do dowodzenia calkowitej poprawnosci programow konieczne sa przeliczalne liczby porzadkowe.
(nie odbylo sie)
Najblizsze seminarium dotyczyc bedzie strukturalnej semantyki operacyjnej (SOS). Sluzy ona do opisu semantyki jezykow programowania. Pomysl polega na podaniu zbioru aksjomatow i regul wnioskowania specyfikujacych semantyke jezyka, przy czy powyzsze aksjomaty i reguly maja bezposrednio wynikac ze struktury jezyka, tzn. jego skladni. Dzieki temu mozna uzyskac prosta, intuicyjna semantyke danego jezyka programowania. Tak naprawde to opowiem o Semantyce Naturalnej powstalej pod wplywem SOS zaproponowanej przez Gordona Plotkina.
(przeniesione z 30.10.97)
Na seminarium zamierzam wprowadzic ogolne zalozenia dotyczace powstajacego jezyka. Szczegolny nacisk zamierzam polozyc na dziedziczenie oraz zwiazane z nim pseudo-zmienne self i super. Algebra wyrazen zostanie ograniczona do niezbednego minimum.
(przeniesione z 8.01)
Najblizsze seminarium dotyczyc bedzie strukturalnej semantyki operacyjnej (SOS). Sluzy ona do opisu semantyki jezykow programowania. Pomysl polega na podaniu zbioru aksjomatow i regul wnioskowania specyfikujacych semantyke jezyka, przy czy powyzsze aksjomaty i reguly maja bezposrednio wynikac ze struktury jezyka, tzn. jego skladni. Dzieki temu mozna uzyskac prosta, intuicyjna semantyke danego jezyka programowania. Tak naprawde to opowiem o Semantyce Naturalnej powstalej pod wplywem SOS zaproponowanej przez Gordona Plotkina.