How to make ad hoc proof automation less ad hoc

DOI10.1145/2034773.2034798zbMath1323.68117OpenAlexW4214826241MaRDI QIDQ5176973

Aleksandar Nanevski, Georges Gonthier, Beta Ziliani, Derek R. Dreyer

Publication date: 5 March 2015

Published in: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.298.3332

zbMATH Keywords

interactive theorem provingCoqtype classestacticscanonical structurescustom proof automationHoare type theory

Mathematics Subject Classification ID

Related Items (6)

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ A Type-Theoretic Approach to Resolution ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ COCHIS: Stable and coherent implicits ⋮ Tactics for Reasoning Modulo AC in Coq

Uses Software

• Coq
• Haskell
• VeriML
• seL4
• Delphin

This page was built for publication: How to make ad hoc proof automation less ad hoc