Coq in a Hurry

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Type de document :
Cours
3rd cycle. Types Summer School, also used at the University of Goteborg, Nice,
Ecole Jeunes Chercheurs en Programmation,
Universite de Nice, France. 2016, pp.49
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://cel.archives-ouvertes.fr/inria-00001173
Contributeur : Yves Bertot <>
Soumis le : jeudi 19 octobre 2017 - 17:34:18
Dernière modification le : mardi 31 octobre 2017 - 01:09:42

Fichiers

coq-hurry.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00001173, version 6

Collections

Citation

Yves Bertot. Coq in a Hurry. 3rd cycle. Types Summer School, also used at the University of Goteborg, Nice,
Ecole Jeunes Chercheurs en Programmation,
Universite de Nice, France. 2016, pp.49. 〈inria-00001173v6〉

Partager

Métriques

Consultations de
la notice

138

Téléchargements du document

95