How to make ad hoc proof automation less ad hoc

From MaRDI portal

Revision as of 01:28, 9 February 2024 by Import240129110113 (talk | contribs) (Created automatically from import240129110113)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:5398327

Jump to:navigation, search

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)

zbMATH Keywords

unification interactive theorem proving Coq proof automation

Mathematics Subject Classification ID

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (5)

Eisbach: a proof method language for Isabelle ⋮ Validating Mathematical Structures ⋮ Unnamed Item ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

Uses Software

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

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:5398327&oldid=20129717"

Pages with script errors