Published June 29, 2016 | Version v1
Publication Metadata-only

Coq in a Hurry

Bertot, Yves
Other:
Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Description

These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on.

Abstract

Expressions and logical formulas
Programming in Coq
Propositions and proofs
Proving properties of programs on numbers
Proving properties of programs on lists
Defining new datatypes
Numbers in the Coq system
Inductive properties

Abstract

3rd cycle

Additional details

Identifiers Origin repository
Created:
March 25, 2023
Modified:
November 29, 2023