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.
Document type :
[Research Report] 2011
Contributor : Andrei Paskevich <>
Submitted on : Tuesday, July 26, 2011 - 12:12:15 PM
Last modification on : Thursday, February 9, 2017 - 4:01:31 PM
Document(s) archivé(s) le : Sunday, December 4, 2016 - 10:19:53 AM


Files produced by the author(s)


  • HAL Id : inria-00591414, version 4



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



Record views


Document downloads