¬ sve za ∀ (no ∃ uvod u propozicije kao tipove)

Nije sve za svakoga (no postoji uvod u propozicije kao tipove) je ovomjesečno izlaganje o konceptu poznatom kao propozicije kao tipovi. To je poveznica između logike i programiranja koju su prepoznali više logičara i računaraca u 20. stoljeću. Izlaganje je kratki uvod u tu poveznicu i preporuka nove knjige pod naslovom Programming Language Foundations in Agda. Prva polovica knjige o kojoj će biti riječ je o logici kroz tipove u smislu matematičke (konstruktivne) logike i teorije tipova.