[Club2] talk by Jasmin Blanchette, June 15, 14:00, Turing

[Andrei Popescu]

Dear All,  
Jasmin will give another talk on June 5 on his and Andrei Paskevich's TFF1, a syntax format for polymorphic problems aimed at automatic theorem provers.  (Notice that Jasmin and Steffen Smolka also have earlier talks, on May 29.)
Best regards,   Andrei 
TFF1: The TPTP Typed First-Order Form with Rank-1 PolymorphismJasmin Blanchette (joint work with Andrei Paskevich)====================================================Wed. June 15, 14:00, MI 00.09.055 ("Alan Turing")
http://www21.in.tum.de/~blanchet/tff1short.pdf
The TPTP World is a well-established infrastructure for automatic theoremprovers. It defines several concrete syntaxes, notably an untyped first-orderform (FOF) and a typed first-order form (TFF0), that have become de factostandards. This paper introduces the TFF1 format, an extension of TFF0 withrank-1 polymorphism. The format is designed to be easy to process by existingreasoning tools that support ML-style polymorphism. It opens the door to usefulmiddleware, such as monomorphizers and other translation tools that encodepolymorphism in FOF or TFF0. Ultimately, the hope is that TFF1 will beimplemented in popular automatic theorem provers.
Warning from Jasmin: 
This is a rehearsal for a CADE talk. This is my second talk at the TUM onthis topic, and there is not much new since last time (except a differentset of slides), so I will not be disappointed if few people show up.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130524/ea012fe7/attachment.html>