wkolowski / coqcat

Formalization of Category Theory in Coq.

Map of all my stuffs / Mapa wszystkich moich rzeczy

EN: Below is a map of my most interesting writings -- books, seminar notes, talk slides (I tend to treat slides just like ordinary notes) and so on. Some of these are in English, while others are in Polish. There are also some links to my most interesting repos.

PL: Poniżej jest mapa moich najbardziej interesujących tekstów -- książek, notatek na seminara, slajdów do wystąpień (slajdy traktuję jak zwykłe notatki), etc. Niektóre są po angielsku, a inne po polsku. Jest też trochę linków do moich najbardziej interesujących repozytoriów.

In English

Theses

• MSc Thesis: Formally verified functional algorithms in Coq (2021, repo)

• BSc Thesis: Formally verified functional programming with monads in Coq (2019, repo)

Seminar talk slides

• Introduction to Dependent Types in F* (2021, repo)

• Coinduction and Topology: an (un)expected connection (2020, repo)

• Coinduction in Type Theory: a quick introduction (2020/2022, repo) - a self-contained version of the above which only deals with the basics of coinduction and omits the topology part, with extra exercises in Coq.

• Algebraic Effects vs Monads in theory and practice (2018, repo)

Seminar talk notes

• Induction in Coq (2017, repo)

Coq projects not related to my theses

• Homotopy Type Theory in Coq (2018)

• Category Theory in Coq (2016)

Research notes

• Type Theory Wishlist (2021-now) - a repo in which I'm trying to invent Frankenstein Type Theory which has all the good things and none of the bad things.

• My research notes on Homotopy Type Theory (2020-now, repo) - my investigation of searchable and separated types in HoTT, inspired by Martin Escardó's "Type Topology".

Other

• Comparison of Proof Assistants - a repo in which I collect code written when learning about proof assistants other than Coq (most recently it's Lean 4).

• My NixOS config

Po polsku

Książka

• Typonomikon (2016-teraz, repo)

Slajdy z wystąpień na seminariach

• Topologiczna analiza danych (2020, repo)

• Homotopiczna teoria typów (2019, repo)

• Logika intuicjonistyczna (2018, repo)

(Interaktywne) notatki

• Coq: jak udowodnić, że nasz program działa poprawnie (2021, repo)

Slajdy do prac dyplomowych

• Slajdy z obrony pracy mag. (2021, repo)

• Slajdy z obrony pracy inż. (2019, repo)

Teksty humanistyczne

• Repo z moimi tekstami "humanistycznymi" (2016, 2018) - jeden o sztucznej inteligencji, dwa o gwarantowanym dochodzie podstawowym