Polymorphic+Typeclass Superposition

Daniel Wand (1, 2)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
2 MPII - Max-Planck-Institut für Informatik

We present an extension of superposition that natively handles a polymorphic type sys-tem extended with type classes, thus eliminating the need for type encodings when used by an interactive theorem prover like Isabelle/HOL. We describe syntax, typing rules, semantics, the polymorphic superposition calculus and an evaluation on a problem set that is generated from Isabelle/HOL theories. Our evaluation shows that native polymor-phic+typeclass performance compares favorably to monomorphisation, a highly efficient but incomplete way of dealing with polymorphism.

Domaines: Logique en informatique [cs.LO]

Daniel Wand. Polymorphic+Typeclass Superposition. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15. ⟨hal-01098078⟩