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.
-
MSc Thesis: Formally verified functional algorithms in Coq (2021, repo)
-
BSc Thesis: Formally verified functional programming with monads in Coq (2019, 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)
- Induction in Coq (2017, repo)
-
Homotopy Type Theory in Coq (2018)
-
Category Theory in Coq (2016)
-
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".
-
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).
- Typonomikon (2016-teraz, repo)
-
Topologiczna analiza danych (2020, repo)
-
Homotopiczna teoria typów (2019, repo)
-
Logika intuicjonistyczna (2018, repo)
-
Slajdy z obrony pracy mag. (2021, repo)
-
Slajdy z obrony pracy inż. (2019, repo)
- Repo z moimi tekstami "humanistycznymi" (2016, 2018) - jeden o sztucznej inteligencji, dwa o gwarantowanym dochodzie podstawowym