Zaawansowane programowanie funkcyjne

Część wykładu Zaawansowane programowanie funkcyjne dotycząca Coqa i Idrisa. Typy w językach programowania służą gwarantowaniu własności programów. Używając typów zależnych możemy formułować bardziej precyzyjne własności i uzyskiwać silniejsze gwarancje. System Coq umożliwia programowanie funkcyjne z typami zależnymi wraz z możliwością automatycznego lub interaktywnego dowodzenia własności programów oraz ich ekstrakcją do języków takich jak Ocaml, Haskell, Scheme. Język Idris jest funkcyjnym językiem programowania z typami zależnymi.

Slajdy do wykładu

wykład 1: Idris
przykładowe pliki
wykład 2: Coq - wstęp
przykładowe pliki: examples.v, mlogic.v, flogic.v
wykład 3: Coq - typowanie i typy indukcyjne
przykładowe pliki: plus.v, lista.v
wykład 4: Coq - zależny pattern matching
przykładowe pliki: match.v
wykład 5: Coq - zależne struktury danych
dodatkowe pliki: head.v, DataStructures.v
wykład 6: Coq - równość
dodatkowe pliki: lastOfNonemptyTuple.v, hastype.v, JMeqDef.v, JMeqRew.v, UIP_refl_nat.v, vappend_assoc.v
wykład 7: Coq - coinductive types
dodatkowe pliki: Coinductive.Casteran.v, Coinductive.cpdt.v, CpdtTactics.vo

Laboratorium

Coq 8.11 jest już zainstalowany na students. Żeby go użyć trzeba najpierw rozszerzyć PATH z przodu o /opt/ocaml/4.09.1/bin (czyli PATH=/opt/ocaml/4.09.1/bin:$PATH) i dopiero potem wywołać coqc lub coqide.

lab 1: Idris
lab 2: Coq - podstawy, logika
lab 3: Coq - typy indukcyjne
lab 4: Coq - zależny pattern matching
lab 5: Coq - zależny pattern matching
lab 6: Coq - zależny pattern matching - dowody z type-cast
lab 7: Coq - coinductive types
Coq assignment

Zaawansowane programowanie funkcyjne

Slajdy do wykładu

Laboratorium

Narzędzia i materiały

wykład:

laboratorium:

materiały 2019