|
|
Open source contribution & experiements (nitpicking):
- Blockchain technologies powered by formal methods: input-output-hk/scrypto, input-output-hk/mantis, ethereum-json-rpc-specification, input-output-hk/metronome
- Agda:
- agda-smash formal specification for Haskell smash library in Agda
- formalverification/milewski-ctfp-pdf WIP translation to Agda of Category Theory for Programmers by Bartosz Milewski
- agda-hott Experiments with HoTT, category theory and FP in Agda
- agda-hott/zio-prelude WIP formalization of zio-prelude in Agda
- agda-verified-fp-algorithms WIP translation of Software Foundations vol 3 : Verified Functional algorithms to Agda
- agda-stdlib
- Haskell input-output-hk/contra-tracer, agda2rust, trifunctors, agda2scala, Haskell wiki, jespercockx/agda2scheme
- Scala FP abstractions inspired by category theory
- Scalaz: day convolution, density commonad, laws for strong profunctor
- cats: laws for strong profunctor
- zio-prelude: Bicovariant, Zivariant, and more
- wiki about FP abstracions inspired by CT scala_typeclassopedia
- exploring differen encodings of category theroy Triglav, applied category theory: svarog
- Scala FP libraries in ZIO ecosystem:
- zio,
- zio-dotty-quickstart.g8, zio-akka-quickstart.g8,
- zio-sql, zio-prelude, zio-json, zio/interop-cats, zio-gcp, zio-config
- Homotopy Type Theory in Agda - ProvingGround
- Idris Idris-Trifunctors, Idris-Applied-Category-Theory
- Purescript: purescript-supermonad
- Racket/Scheme: rackcheck, akeep/rough-draft
- PLT: my collection of resources around Computational Trinitarianism, https://steshaw.org/plt/, yallop/effects-bibliography
Talks:
- Why functional programming and category theory strongly matters, 2019, slides
- Big picture of category theory in scala with deep dive into Contravariant and Profunctors, 2019, slides
- Contravariant functors in scala, 2020, slides, exercises
Study gruops:
- 2023 - Agda - based on PLFA
- 2022 - HoTT/UF in Agda - based on Introduction to Univalent Foundations of Mathematics with Agda - Martín Escardó
- 2020-2021 - Aplied Category Theory - based on 7Sketches and Haskell functional pearls, schedule, attempts to encode in Idris