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.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas: Towards certified meta-programming with typed Template-Coq (2018)
- Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
- Stewart, Gordon; Beringer, Lennart; Appel, Andrew W.: Verified heap theorem prover by paramodulation (2012)
- Huet, Gérard: Axiomatisations, proofs, and formal specifications of algorithms: Commented case studies in the coq proof assistant (1997)
- Dybjer, Peter: Inductive families (1994)
- Huet, Gérard: Residual theory in (\lambda)-calculus: A formal development (1994)