Sciweavers

TYPES
2007
Springer
14 years 5 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...
Pierre Corbineau