| 馃専 | Name | Description | 馃實 |
|---|---|---|---|
| 59 | @sfja/sfja | SoftwareFoundations(Ja) | |
| 57 | @pi8027/lambda-calculus | A Formalization of Typed and Untyped 位-Calculi in Coq and Agda2 | |
| 11 | @pi8027/formalized-postscript | PostScript programming in the Coq proof assistant | |
| 8 | @suharahiromichi/coq | Coq Code | |
| 7 | @amutake/coq-extensible-effects | Extensible Effects in Coq | |
| 7 | @pi8027/efficient-finfun | ||
| 5 | @khibino/sfja-code | Codes for 'Software Foundations' | |
| 4 | @amutake/a-pi | Formalization of A蟺-calculus in Coq | |
| 4 | @yoshihiro503/coqQuickCheck | QuickCheck for Coq | |
| 3 | @OKU1987/FJ_whoas | ||
| 3 | @myuon/CatQ | Formalization of Setoids-enriched Category Theory | |
| 3 | @pi8027/mczify | ||
| 3 | @pi8027/sandpit | ||
| 3 | @yoshihiro503/coqio | Coq IO |