The Gallina specification language. This chapter describes Gallina, the specification language of Coq. It allows developing mathematical theories and to prove specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in theories is described in Section Terms. The language of commands, called The Vernacular is described in Section The Vernacular. In Coq, logical objects are typed to ensure their logical correctness. The rules implemented by the typing algorithm are described in Chapter Calculus of Inductive Constructions.