Encoding monomorphic and polymorphic types

Conference paper

Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2013. Encoding monomorphic and polymorphic types. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Rome 16 - 24 Mar 2013 Springer. pp. 493-507
TypeConference paper
TitleEncoding monomorphic and polymorphic types
AuthorsBlanchette, J., Böhme, S., Popescu, A. and Smallbone, N.
Abstract

Most 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. 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, and partly proved correct, in Isabelle/HOL. Our evaluation finds them vastly superior to previous schemes.

Research GroupFoundations of Computing group
Conference19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Page range493-507
Proceedings TitleTools and Algorithms for the Construction and Analysis of Systems:19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings
SeriesLecture Notes in Computer Science
ISSN0302-9743
Electronic1611-3349
ISBN
Hardcover9783642367410
Electronic9783642367427
PublisherSpringer
Publication dates
Online17 Feb 2013
Print20 Feb 2013
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Accepted author manuscript
File Access Level
Open
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-36742-7_34

Additional information

Published in series title: Lecture Notes in Computer Science, Volume 7795, 2013

Web address (URL)http://dx.doi.org/10.1007/978-3-642-36742-7_34
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/85118

Log in to edit

Download files

Accepted author manuscript
TACAS2013.pdf
File access level: Open

  • 21
    total views
  • 10
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as