Menu

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