Skip to Main content Skip to Navigation
Conference papers

Polymorphic+Typeclass Superposition

Daniel Wand 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, December 22, 2014 - 5:10:12 PM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM
Long-term archiving on: : Monday, March 23, 2015 - 7:41:22 PM


Files produced by the author(s)


  • HAL Id : hal-01098078, version 1



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



Les métriques sont temporairement indisponibles