Cargando…
Hammer for Coq: Automation for Dependent Type Theory
Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundatio...
| Autores principales: | , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
Springer Netherlands
2018
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6044314/ https://www.ncbi.nlm.nih.gov/pubmed/30069074 http://dx.doi.org/10.1007/s10817-018-9458-4 |