Encoding monomorphic and polymorphic types


Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2017. Encoding monomorphic and polymorphic types. Logical Methods in Computer Science. 12 (4). https://doi.org/10.2168/LMCS-12(4:13)2016
TitleEncoding monomorphic and polymorphic types
AuthorsBlanchette, J., Böhme, S., Popescu, A. and Smallbone, N.

Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to un-typed first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of “cover”. The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalized the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.

Research GroupFoundations of Computing group
JournalLogical Methods in Computer Science
Publication dates
Print02 Jan 2017
Publication process dates
Deposited19 May 2015
Submitted14 May 2014
Accepted02 Jan 2017
Output statusPublished
Publisher's version
Digital Object Identifier (DOI)https://doi.org/10.2168/LMCS-12(4:13)2016
Permalink -


Download files

Publisher's version

Restricted files

Accepted author manuscript

  • 24
    total views
  • 0
    total downloads
  • 4
    views this month
  • 0
    downloads this month

Export as