Grupa przedmiotów obieralnych dla informatyki magisterskiej- specjalność Języki programowania (grupa przedmiotów zdefiniowana przez Wydział Matematyki, Informatyki i Mechaniki)
|
Legenda
Jeśli przedmiot jest prowadzony w danym cyklu dydaktycznym, to w odpowiedniej komórce pojawi się koszyk rejestracyjny. Ikona koszyka zależy od tego, czy możesz się rejestrować na dany przedmiot.
- nie jesteś zalogowany 
- aktualnie nie możesz się rejestrować 
- możesz się zarejestrować 
- możesz się wyrejestrować (lub wycofać prośbę) 
- złożyłeś prośbę o zarejestrowanie (i nie możesz jej już wycofać) 
- jesteś pomyślnie zarejestrowany (i nie możesz się wyrejestrować)
Kliknij na ikonę "i" przy koszyku, aby uzyskać dodatkowe informacje.
2024Z - Semestr zimowy 2024/25 2024L - Semestr letni 2024/25 2025Z - Semestr zimowy 2025/26 2025L - Semestr letni 2025/26 (zajęcia mogą być semestralne, trymestralne lub roczne) |
Opcje | |||||||
|---|---|---|---|---|---|---|---|---|
| 2024Z | 2024L | 2025Z | 2025L | |||||
| 1000-2M13LTT |
 
|
brak | brak | brak |
Zajęcia przedmiotu
Semestr zimowy 2024/25
Grupy przedmiotu
Skrócony opis
Wykład obejmie wprowadzenie do różnych systemów z typami i ich interpretacji logicznych w duchu paradygmatu ,,formuły-typy", zwanego też izomorfizmem Curry'ego-Howarda. W szczególności mowa będzie o logice intuicjonistycznej, liniowej i teorio-typowych podstawach wnioskowania wspomaganego komputerowo. |
|
||
| 1000-2N00PLO |
|
brak |
|
brak |
Zajęcia przedmiotu
Semestr zimowy 2024/25
Grupy przedmiotu
Skrócony opis
Celem zajęć jest zapoznanie studentów z podstawami programowania w logice. Na wykładzie zostanie przedstawiona składnia i semantyka (deklaratywna i operacyjna) programów w logice oraz omówiona kwestia poprawności i pełności mechanizmu obliczeniowego stosowanego w programowaniu w logice. Na laboratorium studenci poznają podstawowe techniki programowania w logice. |
|
||
| 1000-2M10PLO | brak |
|
brak |
|
Zajęcia przedmiotu
Semestr letni 2024/25
Grupy przedmiotu
Skrócony opis
Celem zajęć jest pełniejsze przedstawienie programowania w logice (rozszerzenie wiedzy zdobytej na zajęciach z przedmiotu Języki i paradygmaty programowania). Na wykładzie zostanie dokładnie przedstawiony mechanizm obliczeniowy stosowany w programowaniu w logice i zostaną wykazane jego własności (poprawność i pełność). Ponadto zostaną omówione różne semantyki programów z negacją. Na laboratorium studenci poznają techniki programowania w języku Prolog (m.in. dynamiczną modyfikację programu). |
|
||
| 1000-2M02RL | brak | brak |
|
brak |
Zajęcia przedmiotu
Semestr zimowy 2025/26
Grupy przedmiotu
Skrócony opis
Wprowadzenie do rachunku lambda jako abstrakcyjnyego modelu procesu obliczenia. Rachunek bez typów: wlasnosci redukcji, konstrukcja modeli, nierozstrzygalność. Rachunki z typami prostymi i polimorficznymi: normalizacja, siła wyrazu, związki z logiką. |
|
||
| 1000-2M10TKI |
|
brak |
|
brak |
Zajęcia przedmiotu
Semestr zimowy 2024/25
Grupy przedmiotu
Skrócony opis
Algebra ogólna i teoria kategorii to klasyczne juz działy matematyki oferujące abstrakcyjne pojęcia, metody i wyniki, które zaadoptowane zostały przez podstawy informatyki i stanowią dziś standardowy język mówienia między innymi o modelowaniu, projektowaniu i systematycznym konstruowaniu złożonych systemów oprogramowania. Wykład przypomni podstawowe pojęcia algebry ogólnej i od podstaw wprowadzi język teorii kategorii, z konieczności ograniczając sie do pojęć najważniejszych i dotyczących ich podstawowych wyników. Zasygnalizujemy przynajmniej, jak język ten wykorzystywany jest w różnych dziedzinach informatyki, między innymi w teorii typów czy w teorii specyfikacji algebraicznych. Do wykładu przewidziane są ćwiczenia, w praktyce przeplatane z wykładem. Wykład może być prowadzony w języku angielskim, ale w przypadku braku studentów obcojęzycznych, zajęcia zapewne będą prowadzone po polsku. |
|
||
| 1000-2M11ZPF | brak |
|
brak |
|
Zajęcia przedmiotu
Semestr letni 2024/25
Grupy przedmiotu
Skrócony opis
Wykład ma na celu przedstawienie najważniejszych zagadnień nowoczesnego programowania funkcyjnego w językach takich jak Haskell, Coq, Idris ze szczególnym uwzględnieniem wykorzystania typów do specyfikowania i weryfikacji programów. |
|
||
