CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Encoding Monomorphic and Polymorphic Types

Jasmin Christian Blanchette ; Sascha Böhme ; Andrei Popescu ; Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2013, 16-24 March 2013, Rome (0302-9743). Vol. 7795 (2013), p. 493-507.
[Konferensbidrag, refereegranskat]

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.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2013-04-08. Senast ändrad 2013-09-28.
CPL Pubid: 175482

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)