Abstract
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 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. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Corbineau, P. (2008). A declarative language for the Coq proof assistant. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4941 LNCS, pp. 69–84). https://doi.org/10.1007/978-3-540-68103-8_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
