How to make ad hoc proof automation less ad hoc
From MaRDI portal
Publication:5176973
DOI10.1145/2034773.2034798zbMath1323.68117MaRDI 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
interactive theorem proving; Coq; type classes; tactics; canonical structures; custom proof automation; Hoare type theory
68N18: Functional programming and lambda calculus
Related Items
COCHIS: Stable and coherent implicits, Computer Certified Efficient Exact Reals in Coq, A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading, A Type-Theoretic Approach to Resolution, Extensible and Efficient Automation Through Reflective Tactics, Tactics for Reasoning Modulo AC in Coq
Uses Software