Komputerowo wspomagane dowodzenie twierdzeń

(r. ak. 2003/2004)

Prowadzący

Wykład

Aleksy Schubert, piątki 14:15-15:45, sala 5830
Daria Walukiewicz, piątki 14:15-15:45, sala 5830

Laboratorium

Jacek Chrząszcz, strona zajęć

Cel

Poznanie teoretycznych i praktycznych aspektów systemu wspomagania dowodzenia Coq ze szczególnym uwzględnieniem dowodzenia własności programów.

W tym semestrze będziemy się zajmowali wyrażalnością części składowych CoIC (Calculus of Inductive Constructions).

Zasady zaliczania

Wykład

W sesji zimowej odbędzie się egzamin pisemny oraz ustny. Egzamin pisemny będzie polegał na rozwiązywaniu kilku zadań o charakterze matematycznym. Egzamin ustny będzie polegał na przedstawieniu dowodów 3 wybranych przez egzaminowanego twierdzeń.

Laboratorium

Trzeba będzie opracować dowód poprawności krótkiego programu.

Przedmiot

Ocena końcowa będzie obliczana za pomocą jednej z trzech poniższych zasad:

ocena końcowa = ocena z laboratorium,
ocena końcowa = ocena z egzaminu,
ocena końcowa = średnia ważona oceny z laboratorium i oceny z egzaminu.

Wyboru metody oceniania (w tym wag w 3. metodzie) dokonuje sam student. Chcielibyśmy, aby wybór ten był podyktowany przede wszystkim rozstrzygnięciem, w których elementów przedmiotu student się chce uczyć dokładniej. Decyzję co do sposobu zaliczania student ma podjąć i oznajmić prowadzącemu (alx_@_mimuw_edu_pl) najpóźniej do 13.10.2003.

Niezależnie od wybranego sposobu oceniania, ocena będzie mogła zostać wystawiona tylko po uzyskaniu pozytywnego wyniku we wszystkich elementach zaliczenia (wykład i laboratorium).

Egzamin

Termin egzaminu: 26.01.2004, godz. 12:00-15:00
Sala: 3150

Plan wykładu

Wstęp, rachunek lambda bez typów (PS)
Rachunek lambda z typami prostymi - wprowadzenie (PS)
Rachunek lambda z typami prostymi - wyrażalność funkcji (PS)
Rachunek lambda z typami prostymi - złożoność badania równości (PS)

Dotychczasowe notatki w całości (PS)

Wszelkie uwagi prosimy zgłaszać pod adresem: alx@mimuw.edu.pl

Ostatnia modyfikacja: 16.01.2004