Anzeige
Erschienen in:
1997 | OriginalPaper | Buchkapitel
Axiomatisations, Proofs, and Formal Specifications of Algorithms: Commented Case Studies in the Coq Proof Assistant
verfasst von : Gérard Huet
Erschienen in: Logic of Computation
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. It may be obtained by anonymous FTP from site ftp.inria.fr, directory INRIA/coq/Vo. 10. We shall not discuss here in detail how to make proofs in Coq, and refer the interested reader to the Coq Tutorial, in the documentation section of the standard distribution. We shall concentrate in the following lessons on axiomatisations and specifications in the Gallina specification language.