Coq Users' Contributions

Miscellaneous

Coq Extensions

• AACTactics
• Counting
• DescenteInfinie
• MapleMode
• Micromega
• Nfix
• RecursiveDefinition
• ReflexiveFirstOrder
• String

Coq Extensions and Computer Science

• JProver

Coq Use Examples

• CoinductiveExamples
• CoursDeCoq
• Demos
• Groups
• HistoricalExamples

Extracted Programs

• Additions
• BDDs
• Bertrand
• Buchberger
• CanonBDDs
• Continuations
• CoqInCoq
• Dictionaries
• FOUnify
• FSets
• FiringSquad
• Graphs
• Hardware
• HigmanCF
• HigmanNW
• Huffman
• IPC
• Multiplier
• MutualExclusion
• QArith
• QArithSternBrocot
• Ramsey
• SearchTrees
• Stalmarck
• Tait
• ZChinese
• ZSearchTrees

Logical Puzzles and Entertainment

• Checker
• Coqoban
• Shuffle
• Sudoku