Polymorphic+Typeclass Superposition

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.
Type de document :
Communication dans un congrès
Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01098078
Contributeur : Stephan Merz <>
Soumis le : lundi 22 décembre 2014 - 17:10:12
Dernière modification le : mardi 21 novembre 2017 - 01:19:57
Document(s) archivé(s) le : lundi 23 mars 2015 - 19:41:22

Fichier

draft.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01098078, version 1

Collections

Citation

Daniel Wand. Polymorphic+Typeclass Superposition. Konev, Boris and de Moura, Leonardo and Schulz, Stephan. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Jul 2014, Vienna, Austria. pp.15. 〈hal-01098078〉

Partager

Métriques

Consultations de la notice

247

Téléchargements de fichiers

98