Nie jesteś zalogowany |
Cotygodniowe seminarium badawcze
Lista referatów
-
8 października 2021 12:15
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 …
-
9 września 2013 10:15
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 …
-
3 grudnia 2012 10:15
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 …
-
5 listopada 2012 10:15
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 …
-
28 maja 2012 10:15
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 …
-
14 maja 2012 10:15
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.
-
7 maja 2012 10:15
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] …
-
16 kwietnia 2012 10:15
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 …
-
26 marca 2012 10:15
Artur Zawłocki (Uniwersytet Warszawski)
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 …
-
19 marca 2012 10:15
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.
-
-
20 lutego 2012 10:15
Michał Roman Przybyłek (Uniwersytet Warszawski)
Wariacje na Systemach Logicznych
-
16 stycznia 2012 10:15
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 …
-
9 stycznia 2012 10:15
Patryk Czarnik (Uniwersytet Warszawski)
JVM w Coqu po mojemu czyli faktoryzacja faktoryzacji
Chodzi oczywiście o formalizację w Coqu semantyki maszyny wirtualnej Javy. Ogólnie będzie... jak zwykle, a w szczegółach - jak realizuję operacje na stosie wartości (tzw. stackop) i jakie wnioski z tego wynikają dla całej formalizacji.
-
19 grudnia 2011 10:15
Jerzy Tyszkiewicz (Uniwersytet Warszawski)
Parallel Random Access Machines and Spreadsheets Are
W referacie (po polsku, tytuł i slajdy po angielsku) pokażę, że w arkuszach kalkulacyjnych można nie używając żadnych makr zaimplementować interpreter maszyny PRAM (Parallel Random Access Machine). Wskazuje to zarazem na: 1) Możliwość wyrażania w …
