Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze

Plan referatów/Talks schedule

Lista referatów

  • 2021-10-22, godz. 12:15, 5820

    Paweł Urzyczyn (MIMUW)

    NP-completeness of BCI

    We will see a proof of NP-completness of propositional implicational logic BCI, in which each assumption is used exactly once. ...

  • 2021-10-08, godz. 12:15, 5820

    Aleksy Schubert (MIMUW)

    Nierozstrzygalność semiunifikacji na chuseczce do nosa

    Problem semiunifikacji pojawia się naturalnie w zagadnieniach związanych z typowalnością programów funkcyjnych, w których systemy typów opartych na systemie F. Intuicyjnie chodzi tutaj o typowanie, w którym funkcji w programie staramy się przypisać jak najbardziej o...

  • 2013-09-09, godz. 10:15, 4070

    Kokichi Futatsugi (JAIST-RCSV)

    Generate and check method for invariant verification in CafeOBJ

    Effective coordination of inference (a la theorem proving) and search (a la model checking) is one of the most important and interesting research topics in formal methods.  We have developed several kinds of techniques for coordinating inference and search.The generate and check method is a recent ...

  • 2012-12-03, godz. 10:15, 4790

    Bartosz Zieliński (Uniwersytet Łódzki)

    Maude jako preprocesor SQL

    p, li { white-space: pre-wrap; } Opowiem o pomyśle wykorzystania systemów przepisywania termów jako lepszych makroprocesorów, w szczególności opiszę tworzony obecnie system (na wczesnym etapie rozwoju) reprezentowania zapytań SQL jako termów Maude i jego zastosowanie do generowania SQL-a...

  • 2012-11-05, godz. 10:15, 4790

    Michał R. Przybyłek (Uniwersytet Warszawski)

    Associated Categories

    Pokażę, że z obiektami dowolnej skończenie zupełnej 2-kateorii z  notacją dyskretności, można związać kategorie, tak aby 1-morfizmy  odpowiadały funktorom pomiędzy dowiązanymi kategoriami, 2-morfizmy  naturalnym transformacjom, a dyskretne obiekty dyskretnym (w  klasycznym sensie) k...

  • 2012-05-28, godz. 10:15, 4790

    Jędrzej Fulara (Uniwersytet Warszawski)

    Analiza abstrakcyjna zmiennych numerycznych oraz kontenerów danych

    Tym razem nie opowiem o niczym, czego byście jeszcze nie słyszeli. Referat będzie o abstrakcyjnej interpretacji oraz dziedzinach numerycznych i dziedzinach do analizy zawartości kontenerów danych, takich jak tablice i słowniki. Pojawią się (bez technicznych detali) nasze dziedziny numeryczne...

  • 2012-05-14, godz. 10:15, 4790

    Michał Roman Przybyłek (Uniwersytet Warszawski)

    Moduły nad monadami

    Opowiem o formalnej teorii monad w bikategoriach. W szczególności skupię się na charakteryzacji rezolucji monad za pomocą uniwersalnych modułów i luźnych (ko)stożków....

  • 2012-05-07, godz. 10:15, 4790

    Patryk Czarnik (Uniwersytet Warszawski)

    JVM w Coqu - odcinek i-ty

    Referat o tym, co zwykle, czyli o moich przygodach z formalizacją bajtkodu Javy Coq-u.W najbliższym odcinku:* "właściwie to mam prawie wszystkie instrukcje  operujące wewnątrz ramki" ;),* dowód własności programu z pętlą (suma 2*i-1 dla i:[1..n] = n*n),* machanie rękami na temat uogóln...

  • 2012-04-16, godz. 10:15, 4790

    Patryk Czarnik (Uniwersytet Warszawski)

    Testing of Evolving Protocols

    Prerun przed workshopem "Testing: Academic & Industrial Conference Practice and Research Techniques" (http://www2012.taicpart.org)Abstrakt pracy (wspólnej z J. Chrząszczem, A. Schubertem i A. Tarleckim):  A common assumption for the state-of-the-art methods of protocol testing is that the protoco...

  • 2012-03-26, godz. 10:15, 4790

    Artur Zawłocki (Uniwersytet Warszawski)

    Specyfikacja systemów komponentowych (badania własne)

    Przedstawię podejście do specyfikacji systemów złożonych zewspółbieżnych, komunikujących się synchronicznie komponentów, które umożliwia kompozycjonalną specyfikację i weryfikację (o własnościach systemu można wnioskować na podstawie własności komponentów) oraz wspiera refinem...

Strony