[Club2] talk by Jasmin Blanchette, Wed. March 6 at 2 PM, Turing

[Andrei Popescu]

Dear All,  

The coming Wednesday, Jasmin will give a rehearsal talk for his TACAS presentation on type encodings for Sledgehammer.  

NOTE: The talk widely overlaps with previous Club2 and PUMA talks by Jasmin. Hence people who have never heard him  talk about Sledgehammer's type encodings or have time to kill are especially welcome. The others are also welcome.  :) 

Best regards, 
  Andrei 

Encoding monomorphic and polymorphic types
Joint work with Sascha Böhme, Andrei Popescu, and Nicholas Smallbone
====================================================
Wed. March 6, 14:00, Room 00.09.055 ("Alan Turing")

http://www21.in.tum.de/~blanchet/enc_types_paper.pdf

Most automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research [Claessen et al. CADE 2011] 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, and we extend the approach to rank-1 polymorphism. The new encodings are implemented, and partly proved correct, in Isabelle/HOL. Our evaluation finds them vastly superior to previous schemes.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130228/2c0af088/attachment.html>