W imieniu Dziekana Wydziału serdecznie zapraszamy pracowników oraz studentów na seminarium wydziałowe, które odbędzie się we wtorek 27 lutego o godz. 12:30 w Instytucie Informatyki w sali 119.
Prelegentem będzie Maciej Piróg, adiunkt w Instytucie Informatyki UWr (absolwent naszych studiów informatycznych, doktorat na Oksfordzie, postdoc w KU Leuven), który prowadzi badania w obszarze semantyki formalnej języków programowania, wykorzystując metody algebry uniwersalnej w opisie tzw. efektów obliczeniowych. Wygłosi on wykład pt.
Algebry szyte na miarę efektów.
Przed wykładem o 12:00 Dziekan zaprasza na ciasto i kawę.
Streszczenie:
Dożyliśmy czasów programowania w chmurze, architektur heterogenicznych, systemów masywnie współbieżnych i rozproszenia na astronomiczną skalę. Opanowanie tej złożoności wymaga nowych pomysłów na sztukę tworzenia oprogramowania na poziomie wzorców, konwencji, języków programowania, bibliotek i systemów. Szczelne abstrakcje, które do niedawna były mrzonką bujających w obłokach idealistów, stają się codzienną koniecznością zwykłego programisty.
Popularność zyskują pomysły pochodzące ze świata programowania funkcyjnego, takie jak czystość czy bezstanowość. Podczas tej prezentacji zajmiemy się ich bardziej świadomym rozwinięciem: teorią efektów obliczeniowych, czyli tym, co, prócz przetworzenia danych wejściowych na dane wyjściowe, wolno danemu komponentowi: Czy wolno mu zgłosić wyjątek? A może wolno mu porozmawiać z bazą danych? Jednym z podejść do tematu są tzw. efekty algebraiczne, które powstały na przecięciu teorii języków programowania, algebry uniwersalnej i teorii kategorii. Rozwiązują one w elegancki sposób kilka znanych od dekad problemów związanych z efektami, np. problem definiowania nowych efektów przez użytkownika, składania efektów ze sobą, statycznych gwarancji bez konieczności uciekania się do nienaturalnego stylu programowania z monadami.
Punktem wyjścia będzie algebraiczność efektów, czyli odpowiedniość między efektami a odpowiednio rozumianymi teoriami algebraicznymi. Już najprostsze teorie odpowiadają podstawowym efektom: przemienne monoidy odpowiadają programom z niedeterminizmem, (uogólnione) pasy to czytanie ze środowiska, a moduły nad monoidami to zapisywanie. Można więc badać istniejące i definiować nowe efekty przez pryzmat algebry. Podczas prezentacji opowiem nie tylko o tych klasycznych konstrukcjach, ale także o nowszych wynikach, np. o tym, jak pewne pozornie niealgebraiczne konstrukcje można opisywać tzw. algebrami z zakresami [Piróg, Schrijvers, Wu, Jaskelioff, LICS 2018] czy o pierwszej równościowej teorii niedeterminizmu z globalnym stanem [Piróg, Polesiuk, Sieczkowski, FOSSACS 2019].