A: Wstęp

• Cel
• Wybór
• Programowanie i dowodzenie
• Filozofia i matematyka
• Literatura
• Sprawy techniczne

B: Logika

• Logika klasyczna i konstruktywna
• Dedukcja naturalna i taktyki
• Konstruktywny rachunek zdań
• Konstruktywny rachunek kwantyfikatorów
• Paradoks golibrody
• Paradoks pieniądza i kebaba
• Kombinatory taktyk
• Zadania
• Paradoks pijoka
• Ściąga
• Konkluzja

C: Podstawy teorii typów [TODO]

• Typy i termy
• Typy i termy, kanoniczność i uzasadnienie reguł eliminacji
• Typy a zbiory
• Uniwersa
• Pięć rodzajów reguł
• Metateoria
• Parametryczność

D1: Indukcja i rekursja

• Typy induktywne
• Induktywne zdania i predykaty
• Różne
• Wyższe czary
• Dobre, złe i podejrzane typy induktywne
• "Paradoksy" indukcji (TODO)
• Indukcja matematyczna a indukcja w nauce (TODO)
• Podsumowanie

D2: Rekursja i indukcja

• Rekursja jako najlepszość
• Reguły eliminacji (TODO)
• Jak działa taktyka induction (TODO)
• Rodzaje rekursji
• Rekursja prymitywna (TODO)
• Rekursja monotoniczna
• Rekursja polimorficzna
• Rząd rżnie głupa, czyli o pierwszym i wyższym rzędzie (TODO)
• Rekursja wyższego rzędu (TODO)
• Rekursja strukturalna (TODO)
• Rekursja ogólna
• Rekursja po paliwie
• Rekursja dobrze ufundowana
• Indukcja wykresowa
• Metoda induktywnej dziedziny
• Komenda Function
• Rekursja zagnieżdżona
• Metoda induktywno-rekurencyjnej dziedziny
• Metoda induktywnej dziedziny 2
• Plugin Equations
• Podsumowanie (TODO)

D3: Logika boolowska, rozstrzygalność i reflekcja [TODO]

• Logika boolowska
• Rekordy (TODO)
• Klasy (TODO)
• Rozstrzygalność
• Ślepota boolowska (TODO)
• Reflekcja w małej skali (TODO)

D4: Arytmetyka

• Podstawy
• Proste działania
• Porządek
• Rozstrzygalność
• Dzielenie i podzielność
• Silnia
• Współczynnik dwumianowy (TODO)
• Wzory rekurencyjne (TODO)
• Sumy szeregów (TODO)
• Dyskretny pierwiastek kwadratowy (TODO)

D5: Listy

• Proste funkcje
• Funkcje z predykatem boolowskim
• Sekcja mocno ad hoc
• Bardziej skomplikowane funkcje
• Proste predykaty
• Relacje między listami
• Niestandardowe reguły indukcyjne (TODO)

D6: Więcej list [TODO]

• Predykaty i relacje na listach - znowu (TODO)
• Rozstrzyganie predykatów i relacji na listach (TODO)
• Znajdowanie wszystkich podstruktur (TODO)
• Permutacje (TODO)
• Wut da fuk? (TODO)
• Zbiory jako zdeduplikowane permutacje
• Zbiory jako zdeduplikowane permutacje po raz drugi
• Zbiory za pomocą Exists
• Zbiory za pomocą sąsiednich transpozycji
• Zbiory za pomocą transpozycji
• Permutacje, jeszcze dziwniej

F1: Koindukcja i korekursja [TODO]

• Koindukcja (TODO)
• Ćwiczenia (TODO)

F2: Liczby konaturalne [TODO]

• Zero, następnik i nieskończoność
• Dodawanie
• Porządek
• Minimum i maksimum
• Dzielenie przez 2
• Skończoność i nieskończoność
• Parzystość i nieparzystość
• Odejmowanie (TODO)
• Mnożenie (TODO)
• Koindukcja wzajemna (TODO)
• Liczby naturalne i konaturalne

F3: Strumienie [TODO]

• Bipodobieństwo
• sapp
• map
• zipWith i unzip (TODO)
• Inne funkcje (TODO)
• Predykaty i relacje na strumieniach (TODO)
• Permutacje strumieni
• Permutacje strumieni v2
• Strumienie za pomocą przybliżeń (TODO)
• Pomysł dawno zapomniany: (ko)induktywne specyfikacje funkcji (TODO)

F4: Kolisty [TODO]

• Kolisty nie znaczy okrągły

G1: Zippery, czyli łażenie po drzewach [TODO]

• Predykaty na listach i drzewach - przypomnienie (TODO)
• Indeksowanie drzew (TODO)
• Zippery dla list - chodzenie po linie (TODO)
• Szukanie dziury w typie, czyli różniczkowanie (TODO)
• Zippery dla typów induktywnych (TODO)
• Zippery dla typów koinduktywnych (TODO)

G2: Sorty, uniwersa kodów i programowanie generyczne [TODO]

• Sort SProp, czyli zdania, ale takie jakby inne (TODO)
• Uniwersa kodów a programowanie generyczne
• W-typy (TODO)
• Indeksowane W-typy (TODO)
• M-typy (TODO)
• Indeksowane M-typy?
• Kody (nie, nie do gier)

H2: Funkcje

• Funkcje
• Aksjomat ekstensjonalności
• Odwrotności i izomorfizmy (TODO)
• Skracalność (TODO)
• Injekcje
• Surjekcje
• Bijekcje
• Inwolucje
• Uogólnione inwolucje
• Idempotencja
• Skracalność (TODO)

H3: Relacje

• Relacje binarne
• Identyczność relacji
• Operacje na relacjach
• Rodzaje relacji heterogenicznych
• Rodzaje relacji heterogenicznych v2
• Rodzaje relacji homogenicznych
• Relacje równoważności (TODO)
• Relacje apartheidu (TODO)
• Słabe relacje homogeniczne (TODO)
• Złożone relacje homogeniczne (TODO)
• Domknięcia (TODO)
• Redukcje (TODO)

H: [Nie]równości, ścieżki i przepaście [TODO]

• Ścieżki
• Równość a ścieżki
• Ścieżki w typach induktywnych
• Ścieżki w typach koinduktywnych
• Ścieżki między funkcjami
• Ścieżki w uniwersum
• Protokoły różnicowe
• Izomorfizmy typów (TODO)
• Dziwne aksjomaty i płynące z nich logiki (TODO)
• Parametryczność, a raczej jej brak (TODO)

I1: Ltac — język taktyk

• Zarządzanie celami i selektory
• Podstawy języka Ltac
• Backtracking
• Dopasowanie kontekstu i celu
• Wzorce i unifikacja
• Narzędzia przydatne przy dopasowywaniu
• Inne (mało) wesołe rzeczy
• Konkluzja

I2: Spis przydatnych taktyk

• refine — matka wszystkich taktyk
• Drobne taktyki
• Średnie taktyki
• Taktyki dla równości i równoważności
• Taktyki dla redukcji i obliczeń (TODO)
• Procedury decyzyjne
• Ogólne taktyki automatyzacyjne
• Pierścienie, ciała i arytmetyka
• Zmienne egzystencjalne i ich taktyki (TODO)
• Taktyki do radzenia sobie z typami zależnymi (TODO)
• Dodatkowe ćwiczenia
• Inne języki taktyk
• Konkluzja

K: Złożoność obliczeniowa

• Czas działania programu
• Złożoność obliczeniowa
• Złożoność asymptotyczna
• Duże O
• Duże Theta
• Złożoność typowych funkcji na listach
• Złożoność problemu
• Przyspieszanie funkcji rekurencyjnych
• Podsumowanie

L: Kontynuacje i kontrola [TODO]

• Wstęp
• Defunkcjonalizacja (TODO)
• CPS (TODO)
• CPS i defunkcjonalizacja w służbie rekursji ogonowej (TODO)
• Kodowania Churcha (TODO)
• Kodowania Scotta (TODO)
• Listy różnicowe (TODO)