Logika matematyczna w informatyce

RSS

Cel przedmiotu

Relewantność logiki matematycznej w informatyce stoi w wąskim związku z konstruktywnymi aspektami tej pierwszej. Otóż praca logików nad izomorfizmem Curry’ego-Howarda dała podstawy do narzędzi specyfikacji i konstrukcji programów jak HOL/Isabelle, Lego czy Coq. Te narzędzia są w dniu dzisiejszym używane w produkcji przez wysoko kwalifikowanych profesjonalistów. Cel wykładu jest wprowadzenie studenta w teorię i praktykę tego aspektu informatyki.

Program wykładu

Troch˛e matematyki dyskretnej. Struktura syntaksu: sygnatury, termy, systemy dedukcyjne, indukcja strukturalna. Rachunek lambda nietypowany: termy lambda, alfa-konwersja, kody deBrujina, podstawienie, redukcja, normalizacja. Rachunek lambda typowany: typy proste à la Curry i à la Church, unifikacja, synteza typów. Dedukcja naturalna: jednotypowana logika zdaniowa, izomorfizm Curry’ego-Howarda. Wielotypowana logika predykatów pierwszego stopnia: reguły strukturalne, logika równościowa, logika zdaniowa, reguły intuicjonistyczne i klasyczne, kwantyfikatory. Wprowadzenie do Calculus of Constructions i do Coq’a. Semantyka: kraty, algebry Heytinga, algebry Boole’a, elementy teorii kategorii

Charakterystyka pozostałych zajęć

Lab1: składanie lambda-termów (w Ocaml’u); Lab2: kody deBrujin’a (w Ocaml’u); Lab3: synteza typów lambda-termów (w Ocaml’u); Lab4: taktyki dla dowodów równa´n, zda´n i predykatów (w Coq’u); Lab5: taktyki dla dowodów indukcja˛, typy induktywne, dowody właściwości funkcji rekurencyjnych (w Coq’u); Lab6: ekstrakcja programów z dowodów (w Coq’u).

Bibliografia

1. “The Coq proof assistant version 8.2 reference manual”, The Coq Development Team, http://coq.inria.fr/refman/;
2. “Interactive Theorem Proving and Program Development (Coq’Art: The Calculus of Inductive Constructions)”, Yves Bertot and Pierre Castéran, Springer 2004, ISBN:978-3-540-20854-9;
3. “Certified programming with dependent types (draft)”, Adam Chlipala, http://adam.chlipala.net/cpdt/.

Wszelkie prawa zastrzeżone © 2010 Katedra Informatyki   |   Akademia Górniczno-Hutnicza   |   Realizacja Creative Bastards