 Nie jesteś zalogowany | zaloguj się |
| Nie jesteś zalogowany | zaloguj się |
2021-10-22, godz. 12:15, 5820
Paweł Urzyczyn (MIMUW)
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)
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)
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)
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)
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)
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...
