Zakład Języków Programowania
Zakład Języków Programowania prowadzi badania naukowe w zakresie teoretycznych podstaw oraz formalnej semantyki języków programowania, analizy i weryfikacji programów, a także automatycznego dowodzenia twierdzeń. W pracach zespołu wykorzystywane są metody logiki matematycznej oraz algebry uniwersalnej, a także narzędzia takie jak implementacje języków funkcyjnych oraz systemy wspomagające dowodzenie twierdzeń. Projekty naukowe realizowane przez zespół dotyczą następujących tematów:
- metody wnioskowania o programach w rozstrzygalnych fragmentach logiki
- weryfikacja dedukcyjna programów współbieżnych
- semantyka kategoryczna języków programowania z efektami obliczeniowymi
- semantyka operacyjna języków wyższego rzędu
- metody wnioskowania o równoważności programów w językach wyższego rzędu
- transformacje programów
- izomorfizm Curry'ego-Howarda dla logiki klasycznej oraz logik modalnych
- systemy typów i efektów
- automatyczne dowodzenie twierdzeń w logice klasycznej z funkcjami częściowymi
- rezolucja geometryczna