A Declarative Language for the Coq Proof Assistant

This paper presents a new proof language for the Coq proof assistant. This language uses the declarative style. It aims at providing a simple, natural and robust alternative to the existing Ltac tactic language. We give the syntax of our language, an informal description of its commands and its operational semantics. We explain how this language can be used to implement formal proof sketches. Finally, we present some extra features we wish to implement in the future.

• Type: Conference
• Year: 2007
• Where: TYPES
• Authors: Pierre Corbineau
• Keywords: Coq Proof Assistant, Formal Methods, Formal Proof Sketches, Ltac Tactic Language, TYPES 2007