Ogłoszenia Wykłady i zadania Inne materiały
Plan wykładu:
  1. [26.02.2013] Wprowadzenie.
  2. [05.03.2013] Wstęp do Coqa. (Proste przykłady.)
  3. [12.03.2013] Indukcyjne typy danych. (Proste przykłady.)
  4. [19.03.2013] Indukcyjne typy danych, cd. (Przykłady.)
  5. [26.03.2013] Predykaty definiowane indukcyjnie. (Przykłady.)
  6. [09.04.2013] Indukcyjne typy zależne. (Przykłady.)
  7. [16.04.2013] Specyfikacje i typy podzbiorowe. (Przykłady.)
  8. [23.04.2013] Język taktyk Ltac. (Przykłady.)
  9. [30.04.2013] Dowodzenie przez refleksję. (Przykłady.)
  10. [07.05.2013] Koindukcja.
    X.Leroy, H.Grall, "Coinductive big-step operational semantics" (skrypty w Coqu)
    D. Sangiorgi, "On the Origins of Bisimulation and Coinduction"
  11. [14.05.2013] Rekursja ogólna.
    (Definicje dobrze ufundowane. Modelowanie nieterminacji.)
  12. [21.05.2013] Równość heterogeniczna.
    (Przykłady1 Przykłady2.)
    C. McBride, "Elimination with a Motive"
  13. [28.05.2013] Do poczytania: P. Castéran, M. Sozeau, "A Gentle Introduction to Typeclasses and Relations in Coq"
Listy zadań:
Lista nr 1 (termin oddania: 12.03.2013)
Lista nr 2 (termin oddania: 26.03.2013)
Lista nr 3 (termin oddania: 16.04.2013)
Pierwsza część Listy nr 4 (termin oddania: 30.04.2013)
Druga część Listy nr 4 (termin oddania: 30.04.2013)
Lista nr 5 (termin oddania: 14.05.2013)