Light

Wojciech Kołowski photo

wkolowski Goto Github PK

followers: 13.0 following: 0.0 repos: 32.0 gists: 0.0

Name: Wojciech Kołowski

Type: User

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

Wojciech Kołowski's Projects

aisd

Some algorithms in Rust

algeff

My seminar talk about algebraic effects

amh

Metaheuristic algorithms in Haskell

comparison-of-proof-assistants

coq-algs

Formally verified algorithms in Coq: concepts and techniques

coq-mtl

An mtl-like library for dealing with effects in Coq

coqbookpl

Stabilna wersja alfa mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych dziwnych rzeczach.

coqcat

Formalization of Category Theory in Coq.

dependent-types-and-theorem-proving

Slides and code snippets for a talk I have given in November 2021.

dni-otwarte-2021

Materiały do mojego wystąpienia na Dniach Otwartych II UWr 2021

eopl

Code from the book Essentials of Programming Languages, third edition.

formalsystems

haskellml

My Haskell code for Stanfod's machine learning course from Coursera.

hott

Coq code that helps me learn HoTT.

interesting-type-theory-papers

This will be a list of interesting papers in type theory.

kompilator

Kompilator na JFTT 2016

latex-calculi

litt

Moja prezentacja o Homotopicznej Teorii Typów na seminarium z Logiki i Teorii Typów

nixos-config

My NixOS config

papersformalizations

Some code based on papers I read

research

My research in Type Theory

seminar-bisimulation-and-coinduction

Code and slides for my talk presented at the seminar.

seminar-program-certification-in-coq

Materials from the seminar

seminarium-z-logik-nieklasycznych

spoj

My solutions for some (easy) problems from spoj.com

teksty

topologiczna-analiza-danych

Moja prezentacja o topologicznej analizie danych (chociaż jest bardziej o topologii niż o danych)

twelf

Learning Twelf

type-theory-wishlist

Personal research notes

typonomikon

Źródła mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych takich.

1
2

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.