(includes my work as lemastero)
dependency intelligence, vulnerability metadata, SARIF/SBOM, ecosystem hardening
- cabal-plan-submit Haskell dependency intelligence: GitHub Dependency Submission, cabal-audit SARIF enrichment, dependency paths, direct/transitive classification, deprecated dependency detection
- MangoIV/cabal-audit#70, MangoIV/cabal-audit#73, MangoIV/cabal-audit#75 (WIP)
- haskell/security-advisories#321, haskell/security-advisories#322
- blackheaven/haskell-security-action#8
- scalacenter/sbt-dependency-submission#347, scalacenter/sbt-dependency-submission#346
- skogsbaer/HTF#137, skogsbaer/HTF#138
- haskell-repa/repa#32 (awaits review)
- protolude/protolude#153 (awaits review)
removing deprecated crypto, adding test vectors/docs, modern crypto primitives, ZK/PQ/FHE
- kazu-yamamoto/crypton#73, kazu-yamamoto/crypton#74 (awaits review)
- haskell-cryptography/botan#130, haskell-cryptography/botan#131, haskell-cryptography/botan#132 (reused by 135), haskell-cryptography/botan#133 (awaits review), haskell-cryptography/botan#134 (awaits review)
- mongodb-haskell/mongodb#161 (awaits review)
- l29ah/pontarius-xmpp#5 (awaits review)
- kazu-yamamoto/unix-time#68
- well-typed/cborg#378
- tlepoint/fhe.rs#375 (awaits review), tlepoint/fhe.rs#376 (WIP)
- privacy-ethereum/halo2curves#221 (awaits review), privacy-ethereum/halo2curves#222 (WIP)
secure decentralized infrastructure, reliable networking, ledger tooling, blockchain security
- modern-cryptography-kata modern cryptography used in Cardano and Midnight as executable demos with explicit invariants as property tests, and known exploitation angles as unit tests, addressing the problem of high complexity of research based blockchains
- cardano-scaling/hydra#2550, cardano-scaling/hydra#2547
- IntersectMBO/cardano-base#637, IntersectMBO/cardano-base#656, IntersectMBO/cardano-base#657
- IntersectMBO/io-sim#251
- IntersectMBO/ouroboros-network#5372, IntersectMBO/ouroboros-network#5378 (awaits review)
- IntersectMBO/ouroboros-consensus#2042, IntersectMBO/ouroboros-consensus#1939 (WIP)
- midnightntwrk/midnight-ledger#533
- IntersectMBO/plutus#7680 (WIP)
- input-output-hk/contra-tracer, avieth/contra-tracer#9
- txpipe/pallas#780 (awaits review)
- aiken-lang/aiken#1324 (awaits review)
- input-output-hk/scrypto, input-output-hk/mantis, ethereum-json-rpc-specification, input-output-hk/metronome
verification, correctness, compiler tooling, proof-to-code pipelines
- scala/scala3#25470, scala/scala3#25162, scala/scala3#25662 (awaits review), scala/scala3#25765 (WIP)
- Agda, agda/agda#8491, agda/agda#8493 (in review)
- agda/cubical#1299
- agda-stdlib, agda/agda-stdlib#2965
- Copilot-Language/copilot#737 (awaits review)
- agda2scala WIP Scala 2 and Scala 3 backends for Agda - compile Agda proofs into Scala code
- kframework/k
- 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
- HoTT/book, statebox/awesome-applied-ct, nlab
- 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
- Homotopy Type Theory in Agda - ProvingGround
- https://steshaw.org/plt/, yallop/effects-bibliography
- intellij-unison WIP IntelliJ IDEA plugin for Unison language
- zio-scala3-quickstart.g8 sbt template for Scala with hardened security thanks to types safety from ZIO and GithubActions enforcing best practices
- ekmett/profunctors
- Scalaz: day convolution, density commonad, laws for strong profunctor
- cats: laws for strong profunctor
- zio-prelude: Bicovariant, Zivariant, and more
- zio/zio-protoquill#739 (awaits review)
- sbt/sbt#9086, sbt/sbt#9088
- zio, zio/zio#10618 (WIP), zio/zio#10620
- trifectatechfoundation/sudo-rs#1565 (awaits review)
- clayrat/idris-selective#1
- zio-sql, zio-prelude, zio-json, zio/interop-cats, zio-gcp, zio-config
- scala_typeclassopedia wiki about FP abstractions in Scala
- abstraction for trifunctors: Idris-Trifunctors,
- category-actions encodings of FP abstractions: Functor, Monad, Comonad and their laws in uniform way as actions on category
- Purescript: purescript-supermonad
- exploring different encodings of category theory Scala - Triglav, Idris-Trifunctors, Haskell - trifunctors, applied category theory: svarog, Idris-Applied-Category-Theory
- Racket/Scheme test frameworks: rackcheck, akeep/rough-draft
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 - Applied Category Theory - based on 7Sketches and Haskell functional pearls, schedule, attempts to encode in Idris