Everything is possible for one who believes. Mark 9:23
Like a man building a house, who dug down deep and laid the foundation on rock. When a flood came, the torrent struck that house but could not shake it, because it was well built. Luke 6:48
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 (awaits review)
- haskell/security-advisories#321, haskell/security-advisories#322, haskell/security-advisories#331, haskell/security-advisories#335
- blackheaven/haskell-security-action#8, blackheaven/haskell-security-action#10 (WIP)
- scalacenter/sbt-dependency-submission#347, scalacenter/sbt-dependency-submission#346
- TristanCacqueray/cabal-audit#1
- skogsbaer/HTF#137, skogsbaer/HTF#138
- zio/zio-sbt#846
- zio/zio-http#4354
- midnightntwrk/midnight-docs#1625, midnightntwrk/midnight-sdk#451 (awaits review), midnightntwrk/midnight-js#1586 (awaits review)
removing deprecated crypto, adding test vectors/docs, modern crypto primitives, ZK/PQ/FHE
- kazu-yamamoto/crypton#73, kazu-yamamoto/crypton#74
- 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#376
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/cardano-base#673
- 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, midnightntwrk/midnight-ledger#602 (awaits review)
- IntersectMBO/plutus#7680 (WIP)
- input-output-hk/contra-tracer, avieth/contra-tracer#9
- txpipe/pallas#780
- aiken-lang/aiken#1324
- 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#25765, scala/scala3#25662
- Agda, agda/agda#8491, agda/agda#8493
- agda/cubical#1299
- agda/agda-categories#557 (awaits review)
- wasabi315/aegle#19
- agda-stdlib, agda/agda-stdlib#2965, agda/agda-stdlib#3131
- agda/agda2hs#465
- agda2scala Scala 2 and Scala 3 backends for Agda - compile Agda proofs into Scala code
- WhatisRT/pagda#3
- 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
- sbt/sbt#9086, sbt/sbt#9088
- zio, zio/zio#10618 (WIP), zio/zio#10620
- trifectatechfoundation/sudo-rs#1565
- clayrat/idris-selective#1
- djspiewak/skolems#8 (awaits review)
- zio-sql, zio-prelude, zio-json, zio/interop-cats, zio-gcp, zio-config
- scala_typeclassopedia wiki about FP abstractions in Scala
- Purescript: purescript-supermonad
- exploration abstraction for trifunctors: Idris-Trifunctors, Scala - Triglav, Haskell - trifunctors
- exploring different encodings of category theory, applied category theory: svarog, Idris-Applied-Category-Theory
- Racket/Scheme test frameworks: rackcheck, akeep/rough-draft
- astronomy_lab - learn ML in Python on astronomy data
- contrib-intel - tools to help open source contributions
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