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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01098078
Contributor : Stephan Merz <>
Submitted on : Monday, December 22, 2014 - 5:10:12 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on : Monday, March 23, 2015 - 7:41:22 PM

File

draft.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01098078, version 1

Collections

Citation

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

Share

Metrics

Record views

311

Files downloads

209