The Coq Users' Contributions
A
- a translation
- abr
- abstract interpretation
- addition chains
- ails
- aircraft
- algebra
- algorithms
- almost full sets
- alternating bit protocol
- american mathematical monthly problem 11262
- area method
- arithmetic
- ascii character
- assembly
- assisted proofs
- associative arrays
- automata
- automatic theorem proving
- autorewrite
- avl
- axiomatic
B
- baire space
- balanced trees
- bdd
- bdt
- bertrand's postulate
- between property
- binary decision diagrams
- binary integers
- binary lists
- binary search paradigm
- binary search trees
- binary sequences
- bisimulation
- boolean formula
- borel
- buchberger's algorithm
- burali forti paradox
- bytecode verification
C
- c
- calculus of concurrent process (ccs)
- calculus of constructions
- calculus of inductive constructions
- cardinal
- cases
- categorial grammar
- categorical abstract machine
- category
- category theory
- checker
- chinese remainder
- chou gao zhang
- church rosser
- circuit
- circuits
- classical logic
- co induction
- co inductive types
- co recursion
- coalgebra
- code
- coinductive
- coiteration
- colimit
- collision
- commutation
- comparator circuit
- compilation
- compiler
- computational linguistic
- computationnal reflection
- computer arithmetic
- concrete domains
- concurrency
- conflict
- confluence
- congruence
- constraints
- constructive mathematics
- context
- continuations
- conversion
- coq
- coq modules
- correct by construction
- correctness
- cps
- cryptography
- ctl
- curry howard's isomorphism
- cycle detection
D
- data compression
- data flow analysis
- data structures
- davis putnam
- de bruijn indices
- decision procedure
- decision procedures
- decomposition
- definitions
- denotational semantics
- dependency pair
- dependent types
- dependent types.
- diaconescu paradox
- diameter
- dijkstra weakest pre condition calculus
- dimension one ramsey theorem
- diophantus
- discrete time
- discrete time.
- distance
- distributed algorithms
- dominos
E
- efficient data structures
- equational reasoning
- eratosthene sieve
- euclidian geometry
- euler formula
- exact arithmetic
- examples
- exceptions
- explicit substitution
- exponentiation
- extraction
F
- fano
- fermat
- fermat's little theorem
- field tactic
- filtering
- finger trees
- finite automata
- finite automatas
- finite sets
- finite state machines
- first order logic
- first order unification
- flat
- floating point arithmetic
- floats
- floyd
- formal language theory
- formal verification
- functional programming
- functions
- functor
- functors
- fundamental theorem of algebra
G
- garbage collection
- genus
- geometry
- gilbreath's card trick
- goedel rosser incompleteness logic hilbert
- goodstein sequences
- graph
- graph theory
- graphs
- grobner basis
- group theory
H
- hardware verification
- hedges
- high school
- higher order logic
- higher order syntax
- higman's lemma
- hilbert's axioms
- history of coq
- hoare logic
- homogeneous coordinates model
- horpo
- huffman tree
- hurkens paradox
- hypermap
I
- ieee
- imperative program
- impredicativity
- inclusion exclusion
- inconsistency
- inductive
- inequalities
- infinite descent
- infinite transition systems
- integers
- interpretation
- intervals
- intuitionistic choice operator
- intuitionistic logic
- intuitionistic set theory
- invariants
K
- karatsuba multiplication binary ring
- kildall
- kleene
- kleene algebra
- knuth's algorithm
L
- labelled transitions systems
- lambda calculus
- lambda sigma lift calculus
- lambek calculus...
- lazy evaluation
- lebesgue integral
- lexicographic
- limit
- line formatting
- linear algebra
- linear temporal logic
- list
- lpo
- lévy's cube lemma
M
- manna ness
- maple
- maps
- markov
- mathematics
- matrices
- matrix
- measurability
- measures
- meta linguistics
- metatheory
- modal logic
- modal mu calculus
- model checking
- modular reduction
- module
- modules functors search trees
- monad
- monads
- monotony
- mpo
- multimodal categorial grammars
- multiset
- mutual exclusion
N
- natural deduction
- natural semantics
- natural transformation
- nested datatypes
- newman's lemma
- newman's lemma.
- nonzeno
- normal forms
- normalization
- normalization by evalution
- number theory
O
- operational
- optimization
- orbit
- ordering
- ordinal
- ordinals
- oriented angles
- orthogonality
- otway rees
P
- p automata
- parallel moves lemma
- paths
- pcoq
- performance
- permutative conversions
- peterson's algorithm
- pgm
- pi calculus
- plane geometry
- pocklington
- pointed graphs
- polyhedron
- polymorphic recursion
- polynom
- polynomial ideal
- powerpc
- ppc
- presburger
- primality
- prime numbers
- prism theorem
- probability
- probability theory
- process algebra
- process algebras
- process calculi
- program extraction
- program verification
- projective plane
- prolog
- proof as programs
- proof search
- proof terms
- properties
- propositional logic
- protocols
- pts
- pure lambda calculus
- pure type systems
- push down automatas
- puzzles
Q
R
- randomized algorithms
- rational langages
- rational numbers
- reactive systems
- real calculus
- real numbers
- real time systems
- recursive functions
- red black trees
- reflection
- reflexive tactic
- rem theorem
- residual
- rewriting
- reynolds paradox
- ring
- robinson
- rpo
- rsa
- ruler and compass geometry
S
- safety
- satisfiability
- schroeder bernstein
- search operator
- security filesystem unix mls access control
- semantics
- semiring
- set theory
- setoid
- sigma algebras
- simplification
- sokoban
- sorted lists
- sorting
- spi calculus
- square root approximation
- stabilizer
- steinhaus
- stern brocot
- streams
- string
- subset types
- substitution
- sudoku
- symbolic model checking
- synchronization
- syntax/semantics interface
- system f
- system u
T
- tactic reflection arithmetic non linear
- tait proof
- tarjan
- tarski's fixpoint theorem
- tarski's geometry
- tauto
- tautology checker
- tctl
- teaching
- temporal logic
- term
- termination
- three gap theorem
- time
- timed automatas
- timed graphs
- trajectory
- tree automatas bottom up reflexion terms
- trees
- type soundness
- type theory
- typing
U
- unification
- union find
- up to techniques
V
- validity
- vector
- vectors
W
- weak bisimilarity
- weak bisimulation
- weakest precondition
- weakly final
- well founded
- well founded recursion
- well foundedness
- well quasi ordering
Y
- yokouchi's lemma