Plan zajęć
Lista obecności
Rok akademicki 2009/10:
Plan zajęć
Lista obecności
Wyniki sprawdzianu poprawkowego
Osoby, które otrzymały ocenę niedostateczną na zaliczeniu poprawkowym, mają wyjątkowo szansę na OSTATNIĄ poprawkę. Proszę uzgodnić datę poprawki (może być dowolny dzień w tygodniu lub w weekend w lutym) i przesłać mi ją e-mailowo. Jeśli będę mógł w tym terminie to potwierdzę datę poprawki. W przeciwnym razie spotkamy się na początku marca (co będzie wymagać od Was przedłużenia sesji). Ponadto te osoby które nie zjawiły się na zaliczeniu 6 lutego, proszone są o dostarczenie usprawiedliwienia nieobecności.
Uwaga: Zaliczenie poprawkowe (zarówno z wykładów jak i laboratoriów) odbędzie
się dnia 6 lutego (sobota) o godz. 11:00 w DS 1, sala 223.
Na tej stronie znajduje się opis wykładów i laboratoriów do przedmiotu obieralnego Systemy typów dla języków programowania, dla studentów kierunku informatyka na Politechnice Poznańskiej.
Celem tego przedmiotu jest wprowadzenie do teorii i praktyki języków (lub narzędzi) programowania, które gwarantują (przez użycie metod statycznej weryfikacji opartej na typach) określone, pożądane własności aplikacji i systemów implementowanych z użyciem tych narzędzi. W ogólności są to własności niezawodności i bezpieczeństwa.
Skrypt do wykładów (w bieżącej wersji) dostępny jest w formacie PDF oraz w Postscripcie.
Slajdy na temat F# (+ notatki).
Slajdy na temat systemów typów dla języków
programowania współbieżnego (draft)
Uwaga: Slajdy obejmują materiał tylko do bieżącego wykładu.
Sporo miejsca na wykładach poświecone jest zagadnieniom polimorfizmu i dedukcji typów -- cechom które charakteryzują nowoczesne języki programowania, takie jak ML (lub inne języki z rodziny ML, np. Haskell lub Nemerle) oraz Java (od wersji 1.5 z "generics"). Działanie przykładowych programów w języku ML z typami polimorficznymi, ilustrowane jest na wykładach używając popularnego dialektu ML o nazwie Objective Caml.
W drugiej części wykładów omawiane są przykłady zastosowań systemów typów dla języków współbieżnych i rozproszonych opartych na komunikatach: typowanie kanałów I/O, typy liniowe i regularne, wolność od zakleszczenia (ang. deadlock) oraz komunikacja polimorficzna. Działanie wybranych systemów typów tego rodzaju ilustrowane jest na wykładzie używając Nomadic Pict -- współbieżnego języka do programowania rozproszonego i mobilnego.
Celem zajęć laboratoryjnych jest praktyczne poznanie możliwości jakie dają języki programowania, których konstrukcja opiera się na zaawansowanych systemach typów. W ramach kursu poznawać będziemy Objective Caml (OCaml), który udostępnia nie tylko system modułów, ale także pełne wsparcie dla programowania obiektowego -- wszystko to połączone polimorficznym systemem typów z dedukcją typów. Język OCaml zainspirował Microsoft do opracowania języka F#, wariantu ML dla .NET ze składnią i semantyką podobną do podstawowej części OCaml.
Informacje na temat zajęć laboratoryjnych znajdują się na tej stronie.
Komentarze, sugestie i pytania dotyczące tej strony są mile widziane.