Expressing Polymorphic Types in a Many-Sorted Language

François Bobot 1, 2 Andrei Paskevich 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : In this paper, we study translation from a first-order logic with polymorphic types à la ML (of which we give a formal description) to a many-sorted or one-sorted logic as accepted by mainstream automated theorem provers. We consider a three-stage scheme where the last stage eliminates polymorphic types while adding the necessary "annotations" to preserve soundness, and the first two stages serve to protect certain terms so that they can keep their original unannotated form. This protection allows us to make use of provers' built-in theories and operations. We present two existing translation procedures as sound and complete instances of this generic scheme. Our formulation generalizes over the previous ones by allowing us to protect terms of arbitrary monomorphic types. In particular, we can benefit from the built-in theory of arrays in SMT solvers such as Z3, CVC3, and Yices. The proposed methods are implemented in the Why3 tool and we compare their performance in combination with several automated provers.
Type de document :
Rapport
[Research Report] 2011


https://hal.inria.fr/inria-00591414
Contributeur : Andrei Paskevich <>
Soumis le : mardi 26 juillet 2011 - 12:12:15
Dernière modification le : jeudi 9 février 2017 - 16:01:31
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 10:19:53

Fichier

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

Identifiants

  • HAL Id : inria-00591414, version 4

Collections

Citation

François Bobot, Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language. [Research Report] 2011. <inria-00591414v4>

Partager

Métriques

Consultations de
la notice

254

Téléchargements du document

87