Procrastination: A proof engineering technique

Document Associé À Des Manifestations Scientifiques Année : 2018

(1)

Armaël Guéneau

We present a small Coq library for collecting side conditions and deferring their proof.

Informatique [cs] Langage de programmation [cs.PL]

Fichier principal

procrastination.pdf (49.45 Ko)

Origine : Fichiers produits par l'(les) auteur(s)

https://inria.hal.science/hal-01962659

Soumis le : jeudi 20 décembre 2018-17:16:54

Dernière modification le : mardi 3 octobre 2023-17:18:04

hal-01962659 , version 1 (20-12-2018)

Armaël Guéneau. Procrastination: A proof engineering technique. Coq Workshop 2018, Jul 2018, Oxford, United Kingdom. ⟨hal-01962659⟩

INRIA INRIA2

17 Consultations

112 Téléchargements