Language Descriptions - Tools and Applications
Grammars
Coq in computer science
- Coq
- is an interactive theorem prover allowing the expression of mathematical assertions
- mechanically checks proofs of these assertions
- helps find formal proofs
- extracts a certified program from the constructive proof of its formal specification
- works within the theory of the calculus of inductive constructions - a derivative of the calculus of constructions.
- is not an automated theorem prover
- includes automatic theorem proving tactics and various decision procedures
CategoryComputerArchitecture