Sciweavers

Share
TYPES
2007
Springer

A Declarative Language for the Coq Proof Assistant

10 years 1 months ago
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.
Pierre Corbineau
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TYPES
Authors Pierre Corbineau
Comments (0)
books