Wyniki sprawdzianu z wykładów który odbył się 5 lutego 2011 r.
Wyniki sprawdzianu z wykładów który odbył się 5 lutego 2011 r.
Uwaga: Ostateczna poprawka w sobotę 5 marca o 13:30. Spotykamy się w s. lab. 143
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.
Uwaga: Zaległy wykład (a na nim sprawdzian) odbędzie się dnia 5.02.2011 w godzinach 11:00-13:00 w sali 109 (DS1).
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 dostępny jest w formacie PDF.
Slajdy na temat F# (+ notatki).
Slajdy na temat systemów typów dla języków
programowania współbieżnego (draft)
Uwaga: Materiał nie omawiany w wymiarze godzin na studiach niestacjonarnych.
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 OCaml.
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 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.