How to make ad hoc proof automation less ad hoc
From MaRDI portal
Publication:5398327
DOI10.1017/S0956796813000051zbMath1314.68281MaRDI QIDQ5398327
Beta Ziliani, Georges Gonthier, Derek R. Dreyer, Aleksandar Nanevski
Publication date: 27 February 2014
Published in: Journal of Functional Programming (Search for Journal in Brave)
68N18: Functional programming and lambda calculus
Related Items
Validating Mathematical Structures, Mtac: A monad for typed tactic programming in Coq, A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading, Unnamed Item, Eisbach: a proof method language for Isabelle
Uses Software