Expressing Polymorphic Types in a Many-Sorted Language - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2011

Expressing Polymorphic Types in a Many-Sorted Language

Résumé

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.
Fichier principal
Vignette du fichier
polyfol.pdf (646.45 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00591414 , version 1 (09-05-2011)
inria-00591414 , version 2 (09-05-2011)
inria-00591414 , version 3 (11-07-2011)
inria-00591414 , version 4 (26-07-2011)

Identifiants

  • HAL Id : inria-00591414 , version 4

Citer

François Bobot, Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language. [Research Report] 2011. ⟨inria-00591414v4⟩
284 Consultations
325 Téléchargements

Partager

Gmail Facebook X LinkedIn More