Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

10

TYPES
2007
Springer

favoriteEmaildiscussreport

148views Formal Methods» more TYPES 2007»

A Declarative Language for the Coq Proof Assistant

13 years 10 months ago

A Declarative Language for the Coq Proof Assistant

Download rsg.informatik.uni-kl.de

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

Real-time Traffic

Coq Proof Assistant | Formal Methods | Formal Proof Sketches | Ltac Tactic Language | TYPES 2007 |

claim paper

Related Content

» A Framework for Verifying DataCentric Protocols

» Proof Contexts with Late Binding

» Formal Verification of a C Compiler FrontEnd

» Formal Verification of a Clike Memory Model and Its Uses for Verifying Program Transformat...

» Procedural Representation of CIC Proof Terms

» A Proof Dedicated MetaLanguage

» Extracting a Data Flow Analyser in Constructive Logic

» Modular development of certified program verifiers with a proof assistant

» A Coq Library for Verification of Concurrent Programs

Post Info
More Details (n/a)

Added	09 Jun 2010
Updated	09 Jun 2010
Type	Conference
Year	2007
Where	TYPES
Authors	Pierre Corbineau

Comments (0)