Nie jesteś zalogowany |
Logika w informatyce
Opis
Teoria typów w odniesieniu do programowania funkcyjnego, przepisywanie termów, automatyczne wspomaganie dowodzenia. Logiczne podstawy weryfikacji: logika temporalna, logika programów, logika monadyczna i jej związek z automatami i grami. Tematy badawcze dotyczą między innymi siły wyrazu rozmaitych rachunków logicznych, rozstrzygalności, oraz efektywności weryfikacji modelowej.
Seminaria
Pracownicy i doktoranci
-
dr Marcin Benke
Rachunek lambda, teoria typów
-
prof. dr hab. Mikołaj Bojańczyk
Logiki dla weryfikacji, teoria automatów
-
dr Jacek Chrząszcz
Rachunek lambda, przepisywanie termów, systemy wspomagania dowodzenia
- dr hab. Lorenzo Clemente
- dr hab. Wojciech Czerwiński, prof. UW
- dr Tomasz Gogacz
- dr Piotr Hofman
- dr hab. Eryk Kopczyński
-
prof. dr hab. Sławomir Lasota
Weryfikacja, sprawdzanie równoważności, teoria automatów
- dr hab. Filip Murlak, prof. UW
-
dr hab. Anh Linh Nguyen, prof. UW
Logiki modalne, logiki dla baz danych
-
prof. dr hab. Damian Niwiński
Logiki dla weryfikacji, teoria automatów, gry nieskończone, złożoność obliczeniowa
- dr hab. Paweł Parys, prof. UW
-
dr hab. Aleksy Schubert, prof. UW
Rachunek lambda, teoria typów, złożoność systemów logicznych
- dr hab. Michał Skrzypczak
-
prof. dr hab. Andrzej Szałas
Logiki nieklasyczne, wnioskowanie aproksymacyjne, logiki wielowartościowe, automatyczne wnioskowanie, logiki programów, formalna specyfikacja i weryfikacja
-
prof. dr hab. Andrzej Tarlecki
Logika, algebra uniwersalna, teoria kategorii w informatyce
- dr hab. Szymon Toruńczyk, prof. UW
-
prof. dr hab. Jerzy Tyszkiewicz
Logika dla baz danych, teoria modeli skończonych, złożoność Kołmogorowa
-
prof. dr hab. Paweł Urzyczyn
Rachunek lambda, teoria typów, logiki dla weryfikacji
-
dr Daria Walukiewicz-Chrząszcz
Rachunek lambda, przepisywanie termów
