Organizers

dr hab. Aleksy Schubert, prof. UW
prof. dr hab. Andrzej Tarlecki
prof. dr hab. Paweł Urzyczyn

Information

Fridays, 12:15 p.m. , room: 5450

Research fields

List of talks

Oct. 29, 2021, 12:15 p.m.
Aleksy Schubert (MIMUW)
NP-completeness of BCI - another view
Another proof of NP-hardness of provability in BCI is presented. As a more natural source of the reduction, the one-in-three 3SAT problem is assumed.
Oct. 22, 2021, 12:15 p.m.
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.
Oct. 8, 2021, 12:15 p.m.
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 …
Sept. 9, 2013, 10:15 a.m.
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 …
Dec. 3, 2012, 10:15 a.m.
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 …
Nov. 5, 2012, 10:15 a.m.
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) kategoriom. Pozwoli to …
May 28, 2012, 10:15 a.m.
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 …
May 14, 2012, 10:15 a.m.
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.
May 7, 2012, 10:15 a.m.
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] …
April 16, 2012, 10:15 a.m.
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 …
March 26, 2012, 10:15 a.m.
Artur Zawłocki (Uniwersytet Warszawski)
badania własne (Specyfikacja systemów komponentowych)
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 refinement specyfikacji (przechodzenie od specyfikacji abstrakcyjnej do …
March 19, 2012, 10:15 a.m.
Tadeusz Sznuk (Uniwersytet Warszawski)
HAHA
Zamierzam powiedzieć mniej więcej to samo, co poprzednio, czyli do czego to narzędzie ma służyć i jak ma działać. Z tą różnicą, że zamiast slajdów będę się posługiwał prototypem implementacji.
March 12, 2012, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Czytelne programowanie
Feb. 20, 2012, 10:15 a.m.
Michał Roman Przybyłek (Uniwersytet Warszawski)
Wariacje na Systemach Logicznych
Jan. 16, 2012, 10:15 a.m.
Bartek Klin (Uniwersytet Warszawski)
Prerun wykładów habilitacyjnych
TEMAT 1: Mądrej głowie dość dwie słowie, czyli dowody probabilistycznie sprawdzalneJak sprawdzić, czy dowód twierdzenia matematycznego jest poprawny, nie czytając go w całości? Dla pewnej klasy problemów i dowodów jest to możliwe. Dowód probabilistycznie sprawdzalny …