Coq's Prolog and application to defining semi-automatic tactics
In: Type Theory Based Tools ; https://hal.science/hal-01671994 ; Type Theory Based Tools, Jan 2017, Paris, France, 2017
Online
Konferenz
Zugriff:
International audience ; We report on a work-in-progress to re-implement Coq's apply tactic in order to embed some form of simple automation. We design it in a declarative way, relying on typeclasses eauto, a tactic which gives access to the proof-search mechanism behind type classes. We qualify this mechanism of " Coq's Prolog " and describe it in a generic way and explain how it can be used to support the construction of automatic and semi-automatic tactics.
| Titel: |
Coq's Prolog and application to defining semi-automatic tactics
|
|---|---|
| Autor/in / Beteiligte Person: | Zimmermann, Théo ; Herbelin, Hugo ; Design, study and implementation of languages for proofs and programs (PI.R2) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS) |
| Link: | |
| Zeitschrift: | Type Theory Based Tools ; https://hal.science/hal-01671994 ; Type Theory Based Tools, Jan 2017, Paris, France, 2017 |
| Veröffentlichung: | HAL CCSD, 2017 |
| Medientyp: | Konferenz |
| Schlagwort: |
|
| Sonstiges: |
|