Polymorphic+Typeclass Superposition - Archive ouverte HAL Access content directly
Conference Papers Year :

Polymorphic+Typeclass Superposition

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
draft.pdf (378.61 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01098078 , version 1 (22-12-2014)

Identifiers

  • HAL Id : hal-01098078 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More