Cargando…

Practical Proof Search for Coq by Type Inhabitation

We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as large a part of the Calculus of Inductive Constructions...

Descripción completa

Detalles Bibliográficos
Autor principal: Czajka, Łukasz
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324019/
http://dx.doi.org/10.1007/978-3-030-51054-1_3