Xia Li-yao — Vaya

advent-of-coq-2018. Advent of Code 2018, in Coq! (https://adventofcode.com/2018)

141

first-class-families. First-class type families

94

generic-random. Generic random generators

80

profunctor-monad. Bidirectional programming in Haskell with monadic profunctors

49

generic-data. Generic data types in Haskell, utilities for GHC.Generics

47

advent-of-coq-2021. Coq

44

metamorph. Monomorphize polymorphic functions for testing

37

system-F. Formalization of the polymorphic lambda calculus and its parametricity theorem

37

rocq-simple-io. IO for Gallina

34

generic-recursion-schemes. Folds for recursive types with GHC Generics

28

generic-data-surgery. Surgery for generic data types

25

bluefin-algae. Algebraic effects in the Bluefin effect system

22

twentyseven. Rubik's cube solver in Haskell

21

coq-ceres. Coq library for serialization to S-expressions

20

unparse-attoparsec. An attoparsec roundtrip

19

quickcheck-higherorder. QuickCheck extension for higher-order properties

19

gradual-eff-paper. TeX

17

roll-your-own-irc-bot. Roll your own IRC bot (2019 version) https://wiki.haskell.org/Roll_your_own_IRC_bot

16

hashislife. C implementation of the Hashlife algorithm

10

boltzmann-samplers. Haskell

10

coq-recursion-schemes. recursion-schemes in Coq

9

show-combinators. Minimalistic Haskell pretty-printing library

9

test-monad-laws. QuickCheck properties for monad classes

7

coq-mtl. Formalized laws for mtl

7

komachi. Parser library in Agda, with coinductive machines and automatic differentiation

6

type-map. Type-indexed maps, or a lightweight record library

6

advent-of-agda-2022. Agda

6

scanf. scanf and printf in Haskell

4

tina. IRC bots

2

coq-itree-io. Interpreter from itree to IO

2

breadcrumbs. Persistent bounded buffers

2

pnmcosparse. Cosparse analysis greedy algorithms

1

one-liner. Constraint-based generics

1

generic-data-th. Type declarations from GHC Generic Reps

1

aeson-benchmarks-scripts. Haskell

1

hedgehog-higherorder. Haskell

1